mathlib

14f20960 - feat(ring_theory/jacobson): generalized nullstellensatz - polynomials over a Jacobson ring are Jacobson (#4962)

feat(ring_theory/jacobson): generalized nullstellensatz - polynomials over a Jacobson ring are Jacobson (#4962) The main statements are `is_jacobson_polynomial_iff_is_jacobson ` and `is_jacobson_mv_polynomial`, saying that `polynomial` and `mv_polynomial` both preserve jacobson property of rings. This second statement is in some sense a general form of the classical nullstellensatz, since in a Jacobson ring the intersection of maximal ideals containing an ideal will be exactly the radical of that ideal (and so I(V(I)) = I.radical). Co-authored-by: Devon Tuma <dtumad@gmail.com>