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