Theorem CategoryTheory.Abelian.Ext.eq_zero_of_projective

Modification history

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.Abelian.Ext.eq_zero_of_projective View on Github →