# mathlib3documentation

algebra.algebraic_card

### 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] [ A] [char_zero A] :
{x : A | x}.infinite
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
@[simp]
theorem algebraic.cardinal_mk_lift_of_infinite (R : Type u) (A : Type v) [comm_ring R] [comm_ring A] [is_domain A] [ A] [infinite R] :
@[protected, simp]
theorem algebraic.countable (R : Type u) (A : Type v) [comm_ring R] [comm_ring A] [is_domain A] [ A] [countable R] :
{x : A | x}.countable
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}
@[simp]
theorem algebraic.cardinal_mk_of_infinite (R A : Type u) [comm_ring R] [comm_ring A] [is_domain A] [ A] [infinite R] :
cardinal.mk {x // x} =