English
Let S be a set of multivariate polynomials over k. Then the common zeros of all polynomials in the ideal generated by S over K coincide with the points where every polynomial in S vanishes.
Русский
Пусть S — множество многочленов над полем k. Тогда множество точек, удовлетворяющих всем полиномам из порожденного ими идеала, совпадает с множством корней всех p в S, то есть с нулевой зоной порожденного идеала.
LaTeX
$$$\operatorname{zeroLocus}(K, \operatorname{span} S) = \{ x \in K^{\sigma} : \forall p \in S, \ aeval_x(p) = 0 \}$$$
Lean4
theorem zeroLocus_span (S : Set (MvPolynomial σ k)) : zeroLocus K (Ideal.span S) = {x | ∀ p ∈ S, aeval x p = 0} :=
eq_of_forall_le_iff fun _ => le_zeroLocus_iff_le_vanishingIdeal.trans <| Ideal.span_le.trans forall₂_swap
