Theorem CategoryTheory.ShortComplex.ShortExact.hasProjectiveDimensionLT_X₃_iff

Modification history

2025-04-22 08:04
Mathlib/CategoryTheory/Abelian/Projective/Dimension.lean
feat(CategoryTheory/Abelian): Ext^0 and Ext-groups when there are enough projectives (#19591) …
Modified CategoryTheory.ShortComplex.ShortExact.hasProjectiveDimensionLT_X₃_iffView on Github →
2025-01-23 19:32
Mathlib/CategoryTheory/Abelian/ProjectiveDimension.lean
feat(CategoryTheory/Abelian): projective dimension (#19604) …
Added CategoryTheory.ShortComplex.ShortExact.hasProjectiveDimensionLT_X₃_iffView on Github →