Commit 2026-04-13 06:55 a861631a
View on Github →refactor: simplify isLocalRing_of_isAdicComplete_maximal (#37788)
This PR simplifies isLocalRing_of_isAdicComplete_maximal in Mathlib/RingTheory/AdicCompletion/LocalRing.lean by using IsLocalRing.of_unique_max_ideal.
It also removes the now-redundant lemma isUnit_iff_notMem_of_isAdicComplete_maximal, switches to the more specific import Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic, and replaces a separately named maximality instance with [m.IsMaximal].
This is a proof refactor only.