aleph0_le_cardinalMk_of_charZero — Mathlib

English

In characteristic zero, the set of elements of A algebraic over R has cardinality at least aleph-null (i.e., is infinite in a countable sense).

Русский

Характеристика ноль, множество элементов A, алгебраически зависимых над R, имеет кардинал как минимумaleph-null (то есть бесконечно счётно).

LaTeX

$$$\aleph_0 \le \#\{ x \in A \mid IsAlgebraic(R, x) \}.$$$

Lean4

theorem aleph0_le_cardinalMk_of_charZero (R A : Type*) [CommRing R] [Ring A] [Algebra R A] [CharZero A] :
    ℵ₀ ≤ #{ x : A // IsAlgebraic R x } :=
  infinite_iff.1 (Set.infinite_coe_iff.2 <| infinite_of_charZero R A)

Похожие утверждения