Theorem CochainComplex.g_shortComplexTruncLEX₃ToTruncGE

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.g_shortComplexTruncLEX₃ToTruncGEView on Github →