Commit 2026-08-13 22:23 41988ebd

View on Github →

feat(RingTheory/Localization/Ideal): generalize IsLocalization.isMaximal_of_isMaximal_disjoint (#41369) This PR generalizes the existing IsLocalization.isMaximal_of_isMaximal_disjoint in RingTheory/Jacobson/Ring to arbitrary localizations.

Estimated changes

Modified Mathlib/RingTheory/Jacobson/Ring.lean

deleted theorem IsLocalization.isMaximal_of_isMaximal_disjoint

added theorem IsLocalization.isMaximal_of_isMaximal_notMem

Modified Mathlib/RingTheory/KrullDimension/Polynomial.lean

Modified Mathlib/RingTheory/Localization/AtPrime/Basic.lean

deleted theorem Ideal.IsMaximal.of_isLocalization_of_disjoint

Modified Mathlib/RingTheory/Localization/Ideal.lean

added theorem IsLocalization.isMaximal_of_isMaximal_disjoint

added theorem IsLocalization.isMaximal_of_isMaximal_under