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.



leanprover-community/mathlib,leanprover-community/mathlib