infinite_of_charZero — Mathlib

English

Let R and A be rings with R commutative and A a ring, together with an algebra structure of A over R and CharZero on A. Then the set of elements of A that are algebraic over R is infinite.

Русский

Пусть R и A — кольца, R коммутативно, имеется структура алгебры A над R и CharZero на A. Тогда множество элементов A, алгебраически зависимых над R, бесконечно.

LaTeX

$$$\{ x \in A \mid IsAlgebraic(R, x) \}\text{ бесконечно}.$$$

Lean4

theorem infinite_of_charZero (R A : Type*) [CommRing R] [Ring A] [Algebra R A] [CharZero A] :
    {x : A | IsAlgebraic R x}.Infinite :=
  by
  letI := MulActionWithZero.nontrivial R A
  exact infinite_of_injective_forall_mem Nat.cast_injective isAlgebraic_nat

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