Commit 2020-11-27 21:26 14f20960

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).