# Documentation

## Mathlib.Algebra.AlgebraicCard

### 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) [] [] [Ring A] [Algebra R A] [] :
{x : A | }.Infinite
theorem Algebraic.aleph0_le_cardinal_mk_of_charZero (R : Type u_1) (A : Type u_2) [] [] [Ring A] [Algebra R A] [] :
theorem Algebraic.cardinal_mk_lift_le_mul (R : Type u) (A : Type v) [] [] [] [Algebra R A] [] :
theorem Algebraic.cardinal_mk_lift_le_max (R : Type u) (A : Type v) [] [] [] [Algebra R A] [] :
@[simp]
theorem Algebraic.cardinal_mk_lift_of_infinite (R : Type u) (A : Type v) [] [] [] [Algebra R A] [] [] :
@[simp]
theorem Algebraic.countable (R : Type u) (A : Type v) [] [] [] [Algebra R A] [] [] :
{x : A | }.Countable
@[simp]
theorem Algebraic.cardinal_mk_of_countable_of_charZero (R : Type u) (A : Type v) [] [] [] [Algebra R A] [] [] [] [] :
theorem Algebraic.cardinal_mk_le_mul (R : Type u) (A : Type u) [] [] [] [Algebra R A] [] :
Cardinal.mk { x : A // }
theorem Algebraic.cardinal_mk_le_max (R : Type u) (A : Type u) [] [] [] [Algebra R A] [] :
Cardinal.mk { x : A // }
@[simp]
theorem Algebraic.cardinal_mk_of_infinite (R : Type u) (A : Type u) [] [] [] [Algebra R A] [] [] :
Cardinal.mk { x : A // } =