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]
:
@[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]
:
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 (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]
:
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 ℵ₀.