Theorem CategoryTheory.hasExt_of_enoughProjectives

Modification history

2025-07-26 23:35
Mathlib/Algebra/Homology/DerivedCategory/Ext/EnoughProjectives.lean
chore: more indentation fixes (#27502) …
Modified CategoryTheory.hasExt_of_enoughProjectivesView 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 CategoryTheory.hasExt_of_enoughProjectivesView on Github →