feat(RingTheory/LocalRing): Krull dimension results for maximal ideal of local ring (#36787)

Adds 1 declaration:

* `IsLocalRing.maximalIdeal_sq_lt`: In a Noetherian local ring of positive Krull dimension, the square of the maximal ideal is a proper subset of the maximal ideal.

Thanks to Dora Kassabova and Leopold Mayer for edit suggestions.

Author: hommmmm

Mathlib/RingTheory/Ideal/KrullsHeightTheorem.lean

@@ -481,3 +481,15 @@ 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]