Commit 2025-04-22 10:22 bfbbb3df

View on Github →

chore(Algebra): the five lemma for modules (#23496) We reprove the five lemma for modules for universe generality, avoiding the import of Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four in otherwise non-category-theoretic files and for ease of application.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/FiveLemma.lean

added theorem AddMonoidHom.bijective_of_surjective_of_bijective_of_bijective_of_injective

added theorem AddMonoidHom.injective_of_surjective_of_injective_of_injective

added theorem AddMonoidHom.surjective_of_surjective_of_surjective_of_injective

added theorem LinearMap.bijective_of_surjective_of_bijective_of_bijective_of_injective

added theorem LinearMap.injective_of_surjective_of_injective_of_injective

added theorem LinearMap.surjective_of_surjective_of_surjective_of_injective