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] [IsDomain R] (L : Type v) [CommRing L] [IsDomain L] [Algebra R L] [Module.IsTorsionFree 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] [IsDomain R] (L : Type v) [CommRing L] [IsDomain L] [Algebra R L] [Module.IsTorsionFree R L] [Algebra.IsAlgebraic R L] : Cardinal.lift.{u, v} (Cardinal.mk L) ≤ max (Cardinal.lift.{v, u} (Cardinal.mk R)) Cardinal.aleph0

theorem Algebra.IsAlgebraic.cardinalMk_le_sigma_polynomial (R : Type u) [CommRing R] [IsDomain R] (L : Type u) [CommRing L] [IsDomain L] [Algebra R L] [Module.IsTorsionFree R L] [Algebra.IsAlgebraic R L] : Cardinal.mk L ≤ Cardinal.mk ((p : Polynomial R) × { x : L // x ∈ p.aroots L })

theorem Algebra.IsAlgebraic.cardinalMk_le_max (R : Type u) [CommRing R] [IsDomain R] (L : Type u) [CommRing L] [IsDomain L] [Algebra R L] [Module.IsTorsionFree R L] [Algebra.IsAlgebraic R L] : Cardinal.mk L ≤ 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 ℵ₀.