Theorem CochainComplex.shortComplexTruncLE_shortExact

Modification history

2025-09-01 08:25
Mathlib/Algebra/Homology/Embedding/CochainComplex.lean
feat(Algebra/Homology): the canonical t-structure on the derived category (#27395)
Added CochainComplex.shortComplexTruncLE_shortExactView on Github →