Commit 2023-05-12 14:23 0b1f3879

View on Github →

feat: port Algebra.Homology.ShortExact.Abelian (#3940)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Homology/ShortExact/Abelian.lean

added def CategoryTheory.LeftSplit.splitting

added def CategoryTheory.RightSplit.splitting

added def CategoryTheory.Splitting.mk''

added def CategoryTheory.Splitting.mk'

added theorem CategoryTheory.isIso_of_shortExact_of_isIso_of_isIso