Commit 2021-03-10 02:23 fad44b9f
View on Github →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.
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.