mathlib3

fee93e96 - feat(ring_theory/*): Various lemmas about ideals, quotients, and localizations (#5046)

feat(ring_theory/*): Various lemmas about ideals, quotients, and localizations (#5046) Lemmas needed for the proof that is_jacobson is preserved under taking polynomials. Co-authored-by: Devon Tuma <dtumad@gmail.com>