Commit 2021-01-16 11:02 55d5564a

feat(ring_theory/jacobson): Generalize proofs about Jacobson rings and polynomials (#5520) These changes are meant to make deriving the classical nullstellensatz from the generalized version about Jacobson rings much easier and much more direct. is_integral_localization_map_polynomial_quotient already exists in the proof of a previous theorem, and this just pulls it out into an independent lemma. polynomial.quotient_mk_comp_C_is_integral_of_jacobson and mv_polynomial.quotient_mk_comp_C_is_integral_of_jacobson are the two main new statements, most of the rest of the changes are just generalizations and reorganizations of the existing theorems.