Cardinality of algebraic extensions #
This file contains results on cardinality of algebraic extensions.
theorem
Algebra.IsAlgebraic.lift_cardinalMk_le_sigma_polynomial
(R : Type u)
[CommRing R]
(L : Type v)
[CommRing L]
[IsDomain L]
[Algebra R L]
[NoZeroSMulDivisors R L]
[Algebra.IsAlgebraic R L]
:
LE.le (Cardinal.mk L).lift (Cardinal.mk ((p : Polynomial R) × Subtype fun (x : L) => Membership.mem (p.aroots L) x))
theorem
Algebra.IsAlgebraic.lift_cardinalMk_le_max
(R : Type u)
[CommRing R]
(L : Type v)
[CommRing L]
[IsDomain L]
[Algebra R L]
[NoZeroSMulDivisors R L]
[Algebra.IsAlgebraic R L]
:
LE.le (Cardinal.mk L).lift (Max.max (Cardinal.mk R).lift Cardinal.aleph0)
theorem
Algebra.IsAlgebraic.cardinalMk_le_sigma_polynomial
(R : Type u)
[CommRing R]
(L : Type u)
[CommRing L]
[IsDomain L]
[Algebra R L]
[NoZeroSMulDivisors R L]
[Algebra.IsAlgebraic R L]
:
LE.le (Cardinal.mk L) (Cardinal.mk ((p : Polynomial R) × Subtype fun (x : L) => Membership.mem (p.aroots L) x))
@[deprecated Algebra.IsAlgebraic.cardinalMk_le_sigma_polynomial (since := "2024-11-10")]
theorem
Algebra.IsAlgebraic.cardinal_mk_le_sigma_polynomial
(R : Type u)
[CommRing R]
(L : Type u)
[CommRing L]
[IsDomain L]
[Algebra R L]
[NoZeroSMulDivisors R L]
[Algebra.IsAlgebraic R L]
:
LE.le (Cardinal.mk L) (Cardinal.mk ((p : Polynomial R) × Subtype fun (x : L) => Membership.mem (p.aroots L) x))
Alias of Algebra.IsAlgebraic.cardinalMk_le_sigma_polynomial
.
theorem
Algebra.IsAlgebraic.cardinalMk_le_max
(R : Type u)
[CommRing R]
(L : Type u)
[CommRing L]
[IsDomain L]
[Algebra R L]
[NoZeroSMulDivisors R L]
[Algebra.IsAlgebraic R L]
:
LE.le (Cardinal.mk L) (Max.max (Cardinal.mk R) Cardinal.aleph0)
The cardinality of an algebraic extension is at most the maximum of the cardinality
of the base ring or ℵ₀
.
@[deprecated Algebra.IsAlgebraic.cardinalMk_le_max (since := "2024-11-10")]
theorem
Algebra.IsAlgebraic.cardinal_mk_le_max
(R : Type u)
[CommRing R]
(L : Type u)
[CommRing L]
[IsDomain L]
[Algebra R L]
[NoZeroSMulDivisors R L]
[Algebra.IsAlgebraic R L]
:
LE.le (Cardinal.mk L) (Max.max (Cardinal.mk R) Cardinal.aleph0)
Alias of Algebra.IsAlgebraic.cardinalMk_le_max
.
The cardinality of an algebraic extension is at most the maximum of the cardinality
of the base ring or ℵ₀
.