mathlib

55d5564a - feat(ring_theory/jacobson): Generalize proofs about Jacobson rings and polynomials (#5520)

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. Co-authored-by: Devon Tuma <dtumad@gmail.com>