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.transcendental.

source

theorem Algebraic.infinite_of_charZero (R : Type u_1) (A : Type u_2) [CommRing R] [IsDomain R] [Ring A] [Algebra R A] [CharZero A] :

{x : A | IsAlgebraic R x}.Infinite

source

theorem Algebraic.aleph0_le_cardinalMk_of_charZero (R : Type u_1) (A : Type u_2) [CommRing R] [IsDomain R] [Ring A] [Algebra R A] [CharZero A] :

Cardinal.aleph0 ≤ Cardinal.mk { x : A // IsAlgebraic R x }

source

@[deprecated Algebraic.aleph0_le_cardinalMk_of_charZero (since := "2024-11-10")]

theorem Algebraic.aleph0_le_cardinal_mk_of_charZero (R : Type u_1) (A : Type u_2) [CommRing R] [IsDomain R] [Ring A] [Algebra R A] [CharZero A] :

Cardinal.aleph0 ≤ Cardinal.mk { x : A // IsAlgebraic R x }

Alias of Algebraic.aleph0_le_cardinalMk_of_charZero.

source

theorem Algebraic.cardinalMk_lift_le_mul (R : Type u) (A : Type v) [CommRing R] [CommRing A] [IsDomain A] [Algebra R A] [NoZeroSMulDivisors R A] :

Cardinal.lift.{u, v} (Cardinal.mk { x : A // IsAlgebraic R x }) ≤ Cardinal.lift.{v, u} (Cardinal.mk (Polynomial R)) * Cardinal.aleph0

source

@[deprecated Algebraic.cardinalMk_lift_le_mul (since := "2024-11-10")]

theorem Algebraic.cardinal_mk_lift_le_mul (R : Type u) (A : Type v) [CommRing R] [CommRing A] [IsDomain A] [Algebra R A] [NoZeroSMulDivisors R A] :

Cardinal.lift.{u, v} (Cardinal.mk { x : A // IsAlgebraic R x }) ≤ Cardinal.lift.{v, u} (Cardinal.mk (Polynomial R)) * Cardinal.aleph0

Alias of Algebraic.cardinalMk_lift_le_mul.

source

theorem Algebraic.cardinalMk_lift_le_max (R : Type u) (A : Type v) [CommRing R] [CommRing A] [IsDomain A] [Algebra R A] [NoZeroSMulDivisors R A] :

Cardinal.lift.{u, v} (Cardinal.mk { x : A // IsAlgebraic R x }) ≤ Cardinal.lift.{v, u} (Cardinal.mk R) ⊔ Cardinal.aleph0

source

@[deprecated Algebraic.cardinalMk_lift_le_max (since := "2024-11-10")]

theorem Algebraic.cardinal_mk_lift_le_max (R : Type u) (A : Type v) [CommRing R] [CommRing A] [IsDomain A] [Algebra R A] [NoZeroSMulDivisors R A] :

Cardinal.lift.{u, v} (Cardinal.mk { x : A // IsAlgebraic R x }) ≤ Cardinal.lift.{v, u} (Cardinal.mk R) ⊔ Cardinal.aleph0

Alias of Algebraic.cardinalMk_lift_le_max.

source

@[simp]

theorem Algebraic.cardinalMk_lift_of_infinite (R : Type u) (A : Type v) [CommRing R] [CommRing A] [IsDomain A] [Algebra R A] [NoZeroSMulDivisors R A] [Infinite R] :

Cardinal.lift.{u, v} (Cardinal.mk { x : A // IsAlgebraic R x }) = Cardinal.lift.{v, u} (Cardinal.mk R)

source

@[deprecated Algebraic.cardinalMk_lift_of_infinite (since := "2024-11-10")]

theorem Algebraic.cardinal_mk_lift_of_infinite (R : Type u) (A : Type v) [CommRing R] [CommRing A] [IsDomain A] [Algebra R A] [NoZeroSMulDivisors R A] [Infinite R] :

Cardinal.lift.{u, v} (Cardinal.mk { x : A // IsAlgebraic R x }) = Cardinal.lift.{v, u} (Cardinal.mk R)

Alias of Algebraic.cardinalMk_lift_of_infinite.

source

@[simp]

theorem Algebraic.countable (R : Type u) (A : Type v) [CommRing R] [CommRing A] [IsDomain A] [Algebra R A] [NoZeroSMulDivisors R A] [Countable R] :

{x : A | IsAlgebraic R x}.Countable

source

@[simp]

theorem Algebraic.cardinalMk_of_countable_of_charZero (R : Type u) (A : Type v) [CommRing R] [CommRing A] [IsDomain A] [Algebra R A] [NoZeroSMulDivisors R A] [Countable R] [CharZero A] [IsDomain R] :

Cardinal.mk { x : A // IsAlgebraic R x } = Cardinal.aleph0

source

@[deprecated Algebraic.cardinalMk_of_countable_of_charZero (since := "2024-11-10")]

theorem Algebraic.cardinal_mk_of_countable_of_charZero (R : Type u) (A : Type v) [CommRing R] [CommRing A] [IsDomain A] [Algebra R A] [NoZeroSMulDivisors R A] [Countable R] [CharZero A] [IsDomain R] :

Cardinal.mk { x : A // IsAlgebraic R x } = Cardinal.aleph0

Alias of Algebraic.cardinalMk_of_countable_of_charZero.

source

theorem Algebraic.cardinalMk_le_mul (R A : Type u) [CommRing R] [CommRing A] [IsDomain A] [Algebra R A] [NoZeroSMulDivisors R A] :

Cardinal.mk { x : A // IsAlgebraic R x } ≤ Cardinal.mk (Polynomial R) * Cardinal.aleph0

source

@[deprecated Algebraic.cardinalMk_le_mul (since := "2024-11-10")]

theorem Algebraic.cardinal_mk_le_mul (R A : Type u) [CommRing R] [CommRing A] [IsDomain A] [Algebra R A] [NoZeroSMulDivisors R A] :

Cardinal.mk { x : A // IsAlgebraic R x } ≤ Cardinal.mk (Polynomial R) * Cardinal.aleph0

Alias of Algebraic.cardinalMk_le_mul.

source

theorem Algebraic.cardinalMk_le_max (R A : Type u) [CommRing R] [CommRing A] [IsDomain A] [Algebra R A] [NoZeroSMulDivisors R A] :

Cardinal.mk { x : A // IsAlgebraic R x } ≤ Cardinal.mk R ⊔ Cardinal.aleph0

Stacks Tag 09GK

source

@[deprecated Algebraic.cardinalMk_le_max (since := "2024-11-10")]

theorem Algebraic.cardinal_mk_le_max (R A : Type u) [CommRing R] [CommRing A] [IsDomain A] [Algebra R A] [NoZeroSMulDivisors R A] :

Cardinal.mk { x : A // IsAlgebraic R x } ≤ Cardinal.mk R ⊔ Cardinal.aleph0

Alias of Algebraic.cardinalMk_le_max.

Stacks Tag 09GK

source

@[simp]

theorem Algebraic.cardinalMk_of_infinite (R A : Type u) [CommRing R] [CommRing A] [IsDomain A] [Algebra R A] [NoZeroSMulDivisors R A] [Infinite R] :

Cardinal.mk { x : A // IsAlgebraic R x } = Cardinal.mk R

source

@[deprecated Algebraic.cardinalMk_of_infinite (since := "2024-11-10")]

theorem Algebraic.cardinal_mk_of_infinite (R A : Type u) [CommRing R] [CommRing A] [IsDomain A] [Algebra R A] [NoZeroSMulDivisors R A] [Infinite R] :

Cardinal.mk { x : A // IsAlgebraic R x } = Cardinal.mk R

Alias of Algebraic.cardinalMk_of_infinite.