Theorem ModuleCat.injectiveDimension_eq_iSup_localizedModule_prime

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_eq_iSup_localizedModule_primeView on Github →