cardinalMk_of_countable_of_charZero

English

If A has characteristic zero, and R is Countable, then the algebraic elements over R in A form a countable set; in particular, their cardinal equals aleph-null.

Русский

Если характеристика A равна нулю, и R счётно, то множество алгебраических над R элементов в A счётно.

LaTeX

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

Lean4

@[simp]
theorem cardinalMk_of_countable_of_charZero [CharZero A] : #{ x : A // IsAlgebraic R x } = ℵ₀ :=
  (Algebraic.countable R A).le_aleph0.antisymm (aleph0_le_cardinalMk_of_charZero R A)

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