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]
:
Cardinal.lift.{u, v} (Cardinal.mk L) ≤ Cardinal.mk ((p : Polynomial R) × { x : L // x ∈ p.aroots L })
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]
:
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]
:
Cardinal.mk L ≤ Cardinal.mk ((p : Polynomial R) × { x : L // x ∈ p.aroots L })
@[deprecated Algebra.IsAlgebraic.cardinalMk_le_sigma_polynomial]
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]
:
Cardinal.mk L ≤ Cardinal.mk ((p : Polynomial R) × { x : L // x ∈ p.aroots L })
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]
:
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]
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]
:
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 ℵ₀.