Theorem CategoryTheory.ShortComplex.mono_homologyMap_iff_up_to_refinements

Modification history

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