eq_zero_of_aeval_eq_zero — Mathlib

English

If x is algebraically independent over R, then the only polynomial p with coefficients in R that evaluates to zero under the aeval map at x is the zero polynomial.

Русский

Если x алгебраически независимо над R, то единственный полином p с коэффициентами в R, который переходит в нуль под отображением aeval по x, есть нулевой полином.

LaTeX

$$$\\text{AlgebraicIndependent } R\\, x \\rightarrow \\forall p : \\mathrm{MvPolynomial}\\, ι\\, R,\\; \\mathrm{MvPolynomial}.aeval (x : ι \\to A)\\, p = 0 \\rightarrow p = 0$$$

Lean4

theorem eq_zero_of_aeval_eq_zero (h : AlgebraicIndependent R x) :
    ∀ p : MvPolynomial ι R, MvPolynomial.aeval (x : ι → A) p = 0 → p = 0 :=
  algebraicIndependent_iff.1 h

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