Theorem DerivedCategory.HomologySequence.mono_homologyMap_mor₁_iff

Modification history

2024-06-09 22:38
Mathlib/Algebra/Homology/DerivedCategory/HomologySequence.lean
feat: the homology sequence of a distinguished triangle in the derived category (#13664) …
Added DerivedCategory.HomologySequence.mono_homologyMap_mor₁_iffView on Github →