Definable Subsets in the language of rings

This file proves that the set of zeros of a multivariable polynomial is a definable subset.

theorem FirstOrder.Ring.mvPolynomial_zeroLocus_definable {ι : Type u_1} {K : Type u_2} [Field K] [CompatibleRing K] (S : Finset (MvPolynomial ι K)) : (⋃ p ∈ S, (fun (m : ι →₀ ℕ) => MvPolynomial.coeff m p) '' ↑p.support).Definable Language.ring (MvPolynomial.zeroLocus (Ideal.span ↑S))