∀ {k : Type u_1} {K : Type u_2} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] {σ : Type u_3}
  (S : Set (MvPolynomial σ k)), MvPolynomial.zeroLocus K (Ideal.span S) = {x | ∀ p ∈ S, (MvPolynomial.aeval x) p = 0}