Theorem DerivedCategory.subsingleton_hom_of_isStrictlyLE_of_isStrictlyGE

Modification history

2025-04-22 08:04
Mathlib/Algebra/Homology/DerivedCategory/Fractions.lean
feat(CategoryTheory/Abelian): Ext^0 and Ext-groups when there are enough projectives (#19591) …
Added DerivedCategory.subsingleton_hom_of_isStrictlyLE_of_isStrictlyGEView on Github →