Theorem IsLocalization.isMaximal_of_isMaximal_under

Modification history

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