Theorem CochainComplex.HomComplex.Cochain.ofHom_injective

Modification history

2023-10-20 14:35
Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
feat: a homotopy of maps of cochain complexes identifies to (-1)-cochains in the complex of homomorphisms (#7656) …
Added CochainComplex.HomComplex.Cochain.ofHom_injectiveView on Github →