def AffineZeroLocus {n : ℕ} (k : Type u_1) [CommRing k] (S : Set (MvPolynomial (Fin n) k)) : Set (Fin n → k)

The affine zero locus V(S) ⊆ k^n of a set S of polynomials: points at which every f ∈ S vanishes.

def IsAffineZariskiClosed {n : ℕ} {k : Type u_1} [CommRing k] (V : Set (Fin n → k)) : Prop

Zariski-closed subset of k^n (Def 1, Lec 1): a set defined as the common zero locus of some collection of polynomials.

@[simp]

theorem mem_affineZeroLocus {n : ℕ} {k : Type u_1} [CommRing k] (S : Set (MvPolynomial (Fin n) k)) (p : Fin n → k) : p ∈ AffineZeroLocus k S ↔ ∀ f ∈ S, (MvPolynomial.aeval p) f = 0

Membership in the affine zero locus unfolds to vanishing of every polynomial in S.

theorem affineZeroLocus_mono {n : ℕ} {k : Type u_1} [CommRing k] {S T : Set (MvPolynomial (Fin n) k)} (h : S ⊆ T) : AffineZeroLocus k T ⊆ AffineZeroLocus k S

The affine zero locus is order-reversing in the polynomial set: a larger set of equations cuts out a smaller closed subset.