chore(RingTheory): rearrange lemma about square of IsLocalRing.maximalIdeal (leanprover-community#39292)

Author: Thmoas-Guan

Mathlib.lean

@@ -6608,6 +6608,7 @@ public import Mathlib.RingTheory.LocalRing.Length
 public import Mathlib.RingTheory.LocalRing.LocalSubring
 public import Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
 public import Mathlib.RingTheory.LocalRing.MaximalIdeal.Defs
+public import Mathlib.RingTheory.LocalRing.MaximalIdeal.Square
 public import Mathlib.RingTheory.LocalRing.Module
 public import Mathlib.RingTheory.LocalRing.NonLocalRing
 public import Mathlib.RingTheory.LocalRing.Quotient

Mathlib/RingTheory/Ideal/KrullsHeightTheorem.lean

@@ -496,15 +496,3 @@ lemma ringKrullDim_le_spanFinrank_maximalIdeal [IsLocalRing R] :
       Ideal.IsPrime.ne_top'))
 
 end Algebra
-
-/-- In a Noetherian local ring of positive Krull dimension,
-the square of the maximal ideal is strictly contained in the maximal ideal. -/
-lemma IsLocalRing.maximalIdeal_sq_lt [IsLocalRing R] (h : 0 < ringKrullDim R) :
-    (IsLocalRing.maximalIdeal R) ^ 2 < IsLocalRing.maximalIdeal R := by
-  refine lt_of_le_of_ne (Ideal.pow_le_self two_ne_zero) fun h_eq => h.ne' ?_
-  have : IsLocalRing.maximalIdeal R = ⊥ :=
-    Submodule.eq_bot_of_le_smul_of_le_jacobson_bot _ _
-      (IsNoetherian.noetherian _)
-      (by rw [Ideal.smul_eq_mul, ← sq]; exact h_eq.symm.le)
-      (IsLocalRing.maximalIdeal_le_jacobson ⊥)
-  rw [← IsLocalRing.maximalIdeal_height_eq_ringKrullDim, this, Ideal.height_bot, WithBot.coe_zero]

Mathlib/RingTheory/LocalRing/MaximalIdeal/Square.lean

@@ -0,0 +1,42 @@
+/-
+Copyright (c) 2026 Nailin Guan. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Nailin Guan
+-/
+module
+
+public import Mathlib.RingTheory.KrullDimension.Field
+public import Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
+public import Mathlib.RingTheory.Nakayama
+
+/-!
+
+# Lemmas about square of maximal ideal of local ring
+
+-/
+
+public section
+
+variable {R : Type*} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
+
+variable (R) in
+lemma IsLocalRing.maximalIdeal_sq_lt_maximalIdeal :
+    maximalIdeal R ^ 2 < maximalIdeal R ↔ ¬ IsField R := by
+  trans ¬ maximalIdeal R ^ 2 = maximalIdeal R
+  · simp [lt_iff_le_and_ne, Ideal.pow_le_self]
+  · rw [IsLocalRing.isField_iff_maximalIdeal_eq, pow_two]
+    refine Iff.not ⟨fun h ↦ ?_, fun h ↦ by simp [h]⟩
+    exact Submodule.eq_bot_of_eq_ideal_smul_of_le_jacobson_annihilator (IsNoetherian.noetherian _)
+      h.symm (maximalIdeal_le_jacobson _)
+
+/-- In a Noetherian local ring of positive Krull dimension,
+the square of the maximal ideal is strictly contained in the maximal ideal. -/
+lemma IsLocalRing.maximalIdeal_sq_lt_of_ringKrullDim_ne_zero (h : ringKrullDim R ≠ 0) :
+    (maximalIdeal R) ^ 2 < maximalIdeal R :=
+  (maximalIdeal_sq_lt_maximalIdeal R).mpr (ringKrullDim_eq_zero_of_isField.mt h)
+
+@[deprecated "Use `IsLocalRing.maximalIdeal_sq_lt_of_ringKrullDim_ne_zero` instead"
+  (since := "2026-05-13")]
+lemma IsLocalRing.maximalIdeal_sq_lt (h : 0 < ringKrullDim R) :
+    (maximalIdeal R) ^ 2 < maximalIdeal R :=
+  IsLocalRing.maximalIdeal_sq_lt_of_ringKrullDim_ne_zero h.ne.symm