Mathlib Changelog
v4
Changelog
About
Github
Theorem
DerivedCategory.from_singleFunctor_obj_projective_eq_zero
Modification history
2025-04-28 06:56
Mathlib/Algebra/Homology/DerivedCategory/Ext/EnoughProjectives.lean
feat(CategoryTheory/Abelian): Ext when there are enough injectives (#23797) …
Deleted
DerivedCategory.from_singleFunctor_obj_projective_eq_zero
View on Github →
2025-04-22 08:04
Mathlib/Algebra/Homology/DerivedCategory/Ext/EnoughProjectives.lean
feat(CategoryTheory/Abelian): Ext^0 and Ext-groups when there are enough projectives (#19591) …
Added
DerivedCategory.from_singleFunctor_obj_projective_eq_zero
View on Github →