Theorem CategoryTheory.hasProjectiveDimensionLT_zero_iff_isZero

Modification history

2025-09-23 17:30
Mathlib/CategoryTheory/Abelian/Projective/Dimension.lean
feat(Algebra/Homology): define projective dimension as a number (#29882) …
Added CategoryTheory.hasProjectiveDimensionLT_zero_iff_isZeroView on Github →