Theorem ModuleCat.localizedModule_hasInjectiveDimensionLE

Modification history

2026-03-18 17:28
Mathlib/RingTheory/LocalProperties/InjectiveDimension.lean
feat(Algebra): injective dimension equal supremum of localized module (#32033) …
Added ModuleCat.localizedModule_hasInjectiveDimensionLEView on Github →