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)