mathlib3 documentation

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.

source
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
source
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] [algebra R A] [char_zero A] :
cardinal.aleph_0 ≤ cardinal.mk {x // is_algebraic R x}
source
theorem algebraic.cardinal_mk_lift_le_mul (R : Type u) (A : Type v) [comm_ring R] [comm_ring A] [is_domain A] [algebra R A] [no_zero_smul_divisors R A] :
(cardinal.mk {x // is_algebraic R x}).lift ≤ (cardinal.mk (polynomial R)).lift * cardinal.aleph_0
source
theorem algebraic.cardinal_mk_lift_le_max (R : Type u) (A : Type v) [comm_ring R] [comm_ring A] [is_domain A] [algebra R A] [no_zero_smul_divisors R A] :
(cardinal.mk {x // is_algebraic R x}).lift ≤ linear_order.max (cardinal.mk R).lift cardinal.aleph_0
source
@[simp]
theorem algebraic.cardinal_mk_lift_of_infinite (R : Type u) (A : Type v) [comm_ring R] [comm_ring A] [is_domain A] [algebra R A] [no_zero_smul_divisors R A] [infinite R] :
(cardinal.mk {x // is_algebraic R x}).lift = (cardinal.mk R).lift
source
@[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
source
@[simp]
theorem algebraic.cardinal_mk_of_countble_of_char_zero (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] [char_zero A] [is_domain R] :
cardinal.mk {x // is_algebraic R x} = cardinal.aleph_0
source
theorem algebraic.cardinal_mk_le_mul (R A : Type u) [comm_ring R] [comm_ring A] [is_domain A] [algebra R A] [no_zero_smul_divisors R A] :
cardinal.mk {x // is_algebraic R x} ≤ cardinal.mk (polynomial R) * cardinal.aleph_0
source
theorem algebraic.cardinal_mk_le_max (R A : Type u) [comm_ring R] [comm_ring A] [is_domain A] [algebra R A] [no_zero_smul_divisors R A] :
cardinal.mk {x // is_algebraic R x} ≤ linear_order.max (cardinal.mk R) cardinal.aleph_0
source
@[simp]
theorem algebraic.cardinal_mk_of_infinite (R A : Type u) [comm_ring R] [comm_ring A] [is_domain A] [algebra R A] [no_zero_smul_divisors R A] [infinite R] :
cardinal.mk {x // is_algebraic R x} = cardinal.mk R