Commit 2024-11-05 19:21 04d1a953

feat(LocalRing/MaximalIdeal/Basic): localization of a Krull dim zero ring (#17549) For theorem LocalRing.not_mem_maximalIdeal: An element x of a commutative local semiring is not contained in the maximal ideal if and only if it is a unit. For noncomputable def nilradmax_localization_IsSelf: Let S be the localization of a commutative semiring R at a submonoid M that does not contain 0. If the nilradical of R is maximal then there is a ring isomorphism between R and S. As discussed on Zulip here: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/PR.20Permission/near/472582165