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