Theorem CochainComplex.HomComplex.Cocycle.ext

Modification history

2025-12-11 08:08
Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
feat(Algebra/Homology): more API for the HomComplex from a single cochain complex (#32461)
Modified CochainComplex.HomComplex.Cocycle.extView on Github →
2023-09-19 07:20
Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
feat: the type of cocycles in the complex of morphisms between cochain complexes (#7201)
Added CochainComplex.HomComplex.Cocycle.extView on Github →