Theorem Ideal.IsMaximal.of_isLocalization_of_disjoint

Modification history

2026-08-13 22:23
Mathlib/RingTheory/Localization/AtPrime/Basic.lean
feat(RingTheory/Localization/Ideal): generalize `IsLocalization.isMaximal_of_isMaximal_disjoint` (#41369) …
Deleted Ideal.IsMaximal.of_isLocalization_of_disjointView on Github →
2026-01-10 16:04
Mathlib/RingTheory/Localization/AtPrime/Basic.lean
feat(RingTheory/KrullDimension): dimension of polynomial ring (#27542) …
Added Ideal.IsMaximal.of_isLocalization_of_disjointView on Github →