Theorem IsLocalization.isMaximal_of_isMaximal_notMem

Modification history

2026-08-13 22:23
Mathlib/RingTheory/Jacobson/Ring.lean
feat(RingTheory/Localization/Ideal): generalize `IsLocalization.isMaximal_of_isMaximal_disjoint` (#41369) …
Added IsLocalization.isMaximal_of_isMaximal_notMemView on Github →