English
Let x be a family of elements of a commutative R-algebra A indexed by a set ι. The family x is algebraically independent over R if and only if the evaluation map that sends each indeterminate corresponding to i ∈ ι to x_i has trivial kernel; equivalently, for every polynomial p in ι indeterminates with coefficients in R, if p evaluated at x equals 0 in A, then p is the zero polynomial.
Русский
Пусть x — семейство элементов A, который является алгебраически независимы над кольцом R, где A — коммутативное R-алгебра. Тогда x алгебраически независимо над R тогда и только тогда, когда отображение вычисления полиномов в A имеет тривиальный ядро; то есть для любого полинома p в переменных ι с коэффициентами в R, если p(x) = 0 в A, то p = 0.
LaTeX
$$$\\text{AlgebraicIndependent } R\\, x \\;\\iff\\; \\forall p : \\mathrm{MvPolynomial}\\, ι\\, R,\\; \\mathrm{MvPolynomial}.aeval (x : ι \\to A)\\, p = 0 \\rightarrow p = 0$$$
Lean4
theorem algebraicIndependent_iff :
AlgebraicIndependent R x ↔ ∀ p : MvPolynomial ι R, MvPolynomial.aeval (x : ι → A) p = 0 → p = 0 :=
injective_iff_map_eq_zero _
