Theorem CategoryTheory.ShortComplex.add_liftCycles

Modification history

2026-03-02 12:12
Mathlib/Algebra/Homology/ShortComplex/Preadditive.lean
feat(CategoryTheory/Abelian): lemmas for diagram chasing in short complexes (#35930)
Added CategoryTheory.ShortComplex.add_liftCyclesView on Github →