Theorem CategoryTheory.ShortComplex.RightHomologyData.homologyIso_hom_comp_rightHomologyIso_inv

Modification history

2024-07-31 03:44
Mathlib/Algebra/Homology/ShortComplex/Homology.lean
chore: backports for leanprover/lean4#4814 (part 9) (#15352) …
Modified CategoryTheory.ShortComplex.RightHomologyData.homologyIso_hom_comp_rightHomologyIso_invView on Github →
2023-09-19 11:09
Mathlib/Algebra/Homology/ShortComplex/Homology.lean
feat: relations between cycles, opcycles and homology of short complexes (#7194)
Added CategoryTheory.ShortComplex.RightHomologyData.homologyIso_hom_comp_rightHomologyIso_invView on Github →