Documentation

Mathlib.RingTheory.Algebraic.Cardinality

Cardinality of algebraic extensions #

This file contains results on cardinality of algebraic extensions.

source
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))
source
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)
source
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))
source
@[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.

source
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 ℵ₀.

Stacks Tag 09GK

source
@[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 ℵ₀.

Stacks Tag 09GK