English
The vanishing ideal of a set V consists of all polynomials that vanish at every point of V.
Русский
Vanishing идеал множества V — это множество полиномов, обращающихся в нуль на каждой точке V.
LaTeX
$$$\\mathrm{vanishingIdeal}(k,V) = \\{ p \\in \\mathrm{MvPolynomial}(\\sigma,k) \\mid \\forall x\\in V,\\; aeval(x,p)=0\\}$$$
Lean4
/-- Ideal of polynomials with common zeroes at all elements of a set -/
def vanishingIdeal (V : Set (σ → K)) : Ideal (MvPolynomial σ k)
where
carrier := {p | ∀ x ∈ V, aeval x p = 0}
zero_mem' _ _ := RingHom.map_zero _
add_mem' {p q} hp hq x hx := by simp only [hq x hx, hp x hx, add_zero, map_add]
smul_mem' p q hq x hx := by simp only [hq x hx, Algebra.id.smul_eq_mul, mul_zero, map_mul]
