Theorem CategoryTheory.ShortComplex.ShortExact.push

Modification history

2026-09-30 10:34
Mathlib/Algebra/Homology/ShortComplex/Pushout.lean
feat(Algebra/Homology/ShortComplex): pullbacks and pushouts of short exact sequences (#44229) …
Added CategoryTheory.ShortComplex.ShortExact.pushView on Github →