Theorem HomologicalComplex.extend.leftHomologyData.lift_d_comp_eq_zero_iff

Modification history

2024-11-30 00:02
Mathlib/Algebra/Homology/Embedding/ExtendHomology.lean
feat(Algebra/Homology/Embedding): the left homology of an extension of homological complexes (#18502) …
Added HomologicalComplex.extend.leftHomologyData.lift_d_comp_eq_zero_iffView on Github →