mathlib3
42bb0c4b - feat(ring_theory/ideal/operations): add first isomorphism theorem for rings and algebras (#6166)

Commit
4 years ago
feat(ring_theory/ideal/operations): add first isomorphism theorem for rings and algebras (#6166) The first isomorphism theorem for commutative rings `quotient_ker_equiv_of_surjective` and algebras `quotient_ker_alg_equiv_of_surjective`.
Parents
Loading