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.

theorem Algebraic.infinite_of_charZero (R : Type u_1) (A : Type u_2) [CommRing R] [IsDomain R] [Ring A] [Algebra R A] [CharZero A] : Set.Infinite {x : A | IsAlgebraic R x}

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 }

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

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

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

@[simp]

theorem Algebraic.countable (R : Type u) (A : Type v) [CommRing R] [CommRing A] [IsDomain A] [Algebra R A] [NoZeroSMulDivisors R A] [Countable R] : Set.Countable {x : A | IsAlgebraic R x}

@[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

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

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

@[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