Theorem DerivedCategory.to_singleFunctor_obj_eq_zero_of_injective

Modification history

2025-04-28 06:56
Mathlib/Algebra/Homology/DerivedCategory/Ext/EnoughInjectives.lean
feat(CategoryTheory/Abelian): Ext when there are enough injectives (#23797) …
Added DerivedCategory.to_singleFunctor_obj_eq_zero_of_injectiveView on Github →