mathlib3 documentation


Cardinality of algebraic numbers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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_char_zero (R : Type u_1) (A : Type u_2) [comm_ring R] [is_domain R] [ring A] [algebra R A] [char_zero A] :
{x : A | is_algebraic R x}.infinite
@[protected, simp]
theorem algebraic.countable (R : Type u) (A : Type v) [comm_ring R] [comm_ring A] [is_domain A] [algebra R A] [no_zero_smul_divisors R A] [countable R] :
{x : A | is_algebraic R x}.countable