Commit 2023-05-12 08:51 30768e35

View on Github →

feat: port CategoryTheory.Abelian.DiagramLemmas.Four (#3935)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Abelian/DiagramLemmas/Four.lean

added theorem CategoryTheory.Abelian.epi_of_epi_of_epi_of_mono

added theorem CategoryTheory.Abelian.isIso_of_isIso_of_isIso_of_isIso_of_isIso

added theorem CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono