From 8af42bb66424fb6e2bd5a950c108e24270a33cda Mon Sep 17 00:00:00 2001 From: Vlad Tsyrklevich Date: Sun, 24 May 2026 10:17:41 +0200 Subject: [PATCH] doc(RingTheory): fix local ring doc comment The predicate for local rings was updated to the current definition on non-commutative semirings back in mathlib3, but the outdated comment stating that local rings are commutative rings with a unique maximal ideal has not been updated since. --- Mathlib/RingTheory/LocalRing/Defs.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Mathlib/RingTheory/LocalRing/Defs.lean b/Mathlib/RingTheory/LocalRing/Defs.lean index 91b664ec848ac3..472f56742e90d8 100644 --- a/Mathlib/RingTheory/LocalRing/Defs.lean +++ b/Mathlib/RingTheory/LocalRing/Defs.lean @@ -12,14 +12,14 @@ public import Mathlib.Algebra.Ring.Defs # Local rings -Define local rings as commutative rings having a unique maximal ideal. +Define the notion of a local ring for non-commutative semirings. In the commutative case, +this is shown to be equivalent to the familiar definition that there exists a unique +maximal ideal in `IsLocalRing.of_unique_max_ideal` and `IsLocalRing.maximal_ideal_unique`. ## Main definitions * `IsLocalRing`: A predicate on semirings, stating that for any pair of elements that - adds up to `1`, one of them is a unit. In the commutative case this is shown to be equivalent - to the condition that there exists a unique maximal ideal, see - `IsLocalRing.of_unique_max_ideal` and `IsLocalRing.maximal_ideal_unique`. + adds up to `1`, one of them is a unit. -/