Theorem CochainComplex.HomComplex.Cochain.fromSingleMk_surjective

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.Cochain.fromSingleMk_surjectiveView on Github →