Theorem ModuleCat.injectiveDimension_le_injectiveDimension_of_isLocalizedModule

Modification history

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