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] :
{x : A | IsAlgebraic R x}.Infinite
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