mathlib documentation

algebra.algebraic_card

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 # polynomial R * ℵ₀.

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

@[simp]
theorem algebraic.countable_of_encodable (R : Type u) (A : Type v) [comm_ring R] [comm_ring A] [is_domain A] [algebra R A] [no_zero_smul_divisors R A] [encodable R] :
{x : A | is_algebraic R x}.countable