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, ⇑p.coeff '' ↑p.support).Definable Language.ring (MvPolynomial.zeroLocus K (Ideal.span ↑S))