Theorem CategoryTheory.hasExt_of_enoughInjectives

Modification history

2025-07-25 22:49
Mathlib/Algebra/Homology/DerivedCategory/Ext/EnoughInjectives.lean
chore: fix more indentation (#27494) …
Modified CategoryTheory.hasExt_of_enoughInjectivesView on Github →
2025-04-28 06:56
Mathlib/Algebra/Homology/DerivedCategory/Ext/EnoughInjectives.lean
feat(CategoryTheory/Abelian): Ext when there are enough injectives (#23797) …
Added CategoryTheory.hasExt_of_enoughInjectivesView on Github →