mathlib

fad44b9f - feat(ring_theory/ideal/operations): add quotient_equiv (#6492)

feat(ring_theory/ideal/operations): add quotient_equiv (#6492) The ring equiv `R/I ≃+* S/J` induced by a ring equiv `f : R ≃+* S`, where `J = f(I)`, and similarly for algebras.