Theorem CochainComplex.HomComplex.Cochain.fromSingleMk_add

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_add View on Github →