Theorem CochainComplex.HomComplex.Cocycle.fromSingleMk_mem_coboundaries_iff

Modification history

2025-12-11 08:08
Mathlib/Algebra/Homology/HomotopyCategory/HomComplexSingle.lean
feat(Algebra/Homology): more API for the HomComplex from a single cochain complex (#32461)
Added CochainComplex.HomComplex.Cocycle.fromSingleMk_mem_coboundaries_iffView on Github →