Documentation

Mathlib.Algebra.AlgebraicCard

Cardinality of algebraic numbers #

In this file, we prove variants of the following result: the cardinality of algebraic numbers under an R-algebra is at most # R[X] * ℵ₀.

Although this can be used to prove that real or complex transcendental numbers exist, a more direct proof is given by Liouville.is_transcendental.

source
theorem Algebraic.infinite_of_charZero (R : Type u_1) (A : Type u_2) [CommRing R] [IsDomain R] [Ring A] [Algebra R A] [CharZero A] :
{x : A | IsAlgebraic R x}.Infinite
source
theorem Algebraic.aleph0_le_cardinal_mk_of_charZero (R : Type u_1) (A : Type u_2) [CommRing R] [IsDomain R] [Ring A] [Algebra R A] [CharZero A] :
Cardinal.aleph0 ≤ Cardinal.mk { x : A // IsAlgebraic R x }
source
theorem Algebraic.cardinal_mk_lift_le_mul (R : Type u) (A : Type v) [CommRing R] [CommRing A] [IsDomain A] [Algebra R A] [NoZeroSMulDivisors R A] :
Cardinal.lift.{u, v} (Cardinal.mk { x : A // IsAlgebraic R x }) ≤ Cardinal.lift.{v, u} (Cardinal.mk (Polynomial R)) * Cardinal.aleph0
source
theorem Algebraic.cardinal_mk_lift_le_max (R : Type u) (A : Type v) [CommRing R] [CommRing A] [IsDomain A] [Algebra R A] [NoZeroSMulDivisors R A] :
Cardinal.lift.{u, v} (Cardinal.mk { x : A // IsAlgebraic R x }) ≤ max (Cardinal.lift.{v, u} (Cardinal.mk R)) Cardinal.aleph0
source
@[simp]
theorem Algebraic.cardinal_mk_lift_of_infinite (R : Type u) (A : Type v) [CommRing R] [CommRing A] [IsDomain A] [Algebra R A] [NoZeroSMulDivisors R A] [Infinite R] :
Cardinal.lift.{u, v} (Cardinal.mk { x : A // IsAlgebraic R x }) = Cardinal.lift.{v, u} (Cardinal.mk R)
source
@[simp]
theorem Algebraic.countable (R : Type u) (A : Type v) [CommRing R] [CommRing A] [IsDomain A] [Algebra R A] [NoZeroSMulDivisors R A] [Countable R] :
{x : A | IsAlgebraic R x}.Countable
source
@[simp]
theorem Algebraic.cardinal_mk_of_countable_of_charZero (R : Type u) (A : Type v) [CommRing R] [CommRing A] [IsDomain A] [Algebra R A] [NoZeroSMulDivisors R A] [Countable R] [CharZero A] [IsDomain R] :
Cardinal.mk { x : A // IsAlgebraic R x } = Cardinal.aleph0
source
theorem Algebraic.cardinal_mk_le_mul (R : Type u) (A : Type u) [CommRing R] [CommRing A] [IsDomain A] [Algebra R A] [NoZeroSMulDivisors R A] :
Cardinal.mk { x : A // IsAlgebraic R x } ≤ Cardinal.mk (Polynomial R) * Cardinal.aleph0
source
theorem Algebraic.cardinal_mk_le_max (R : Type u) (A : Type u) [CommRing R] [CommRing A] [IsDomain A] [Algebra R A] [NoZeroSMulDivisors R A] :
Cardinal.mk { x : A // IsAlgebraic R x } ≤ max (Cardinal.mk R) Cardinal.aleph0
source
@[simp]
theorem Algebraic.cardinal_mk_of_infinite (R : Type u) (A : Type u) [CommRing R] [CommRing A] [IsDomain A] [Algebra R A] [NoZeroSMulDivisors R A] [Infinite R] :
Cardinal.mk { x : A // IsAlgebraic R x } = Cardinal.mk R