# mathlibdocumentation

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.

theorem algebraic.aleph_0_le_cardinal_mk_of_char_zero (R : Type u_1) (A : Type u_2) [comm_ring R] [is_domain R] [ring A] [ A] [char_zero A] :
theorem algebraic.cardinal_mk_lift_le_mul (R : Type u) (A : Type v) [comm_ring R] [comm_ring A] [is_domain A] [ A]  :
(cardinal.mk {x // x}).lift
theorem algebraic.cardinal_mk_lift_le_max (R : Type u) (A : Type v) [comm_ring R] [comm_ring A] [is_domain A] [ A]  :
(cardinal.mk {x // x}).lift
theorem algebraic.cardinal_mk_lift_le_of_infinite (R : Type u) (A : Type v) [comm_ring R] [comm_ring A] [is_domain A] [ A] [infinite R] :
@[simp]
theorem algebraic.countable_of_encodable (R : Type u) (A : Type v) [comm_ring R] [comm_ring A] [is_domain A] [ A] [encodable R] :
{x : A | x}.countable
@[simp]
theorem algebraic.cardinal_mk_of_encodable_of_char_zero (R : Type u) (A : Type v) [comm_ring R] [comm_ring A] [is_domain A] [ A] [encodable R] [char_zero A] [is_domain R] :
theorem algebraic.cardinal_mk_le_mul (R A : Type u) [comm_ring R] [comm_ring A] [is_domain A] [ A]  :
cardinal.mk {x // x}
theorem algebraic.cardinal_mk_le_max (R A : Type u) [comm_ring R] [comm_ring A] [is_domain A] [ A]  :
cardinal.mk {x // x}
theorem algebraic.cardinal_mk_le_of_infinite (R A : Type u) [comm_ring R] [comm_ring A] [is_domain A] [ A] [infinite R] :
cardinal.mk {x // x}