mem_zeroLocus_iff — Mathlib

English

A polynomial p lies in vanishingIdeal k V if and only if p evaluates to zero at every point of V.

Русский

Полином p принадлежит vanishingIdeal k V тогда и только тогда, когда p обращается в нуль в каждой точке V.

LaTeX

$$$p\\in \\mathrm{vanishingIdeal}\\ k\\,V \\iff \\forall x\\in V,\\ aeval(x,p)=0$$$

Lean4

@[simp]
theorem mem_zeroLocus_iff {I : Ideal (MvPolynomial σ k)} {x : σ → K} : x ∈ zeroLocus K I ↔ ∀ p ∈ I, aeval x p = 0 :=
  Iff.rfl

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