Theorem ModuleCat.hasInjectiveDimensionLE_iff_forall_primeSpectrum

Modification history

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