Theorem CochainComplex.HomComplex.Cocycle.cochain_ofHom_homOf_eq_coe

Modification history

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