Commit 2024-02-28 07:39 d6136815
View on Github →feat(Mathlib/RingTheory/Ideal/QuotientOperations): First Isomorphism Theorem for algebras (#11027) We add the First Isomorphism Theorem for algebras. (only the surjective version was present in mathlib). We also adjust the docstring on top of the file.