Lemmas about square of maximal ideal of local ring

theorem IsLocalRing.maximalIdeal_sq_lt_maximalIdeal (R : Type u_1) [CommRing R] [IsLocalRing R] [IsNoetherianRing R] : maximalIdeal R ^ 2 < maximalIdeal R ↔ ¬IsField R

theorem IsLocalRing.maximalIdeal_sq_lt_of_ringKrullDim_ne_zero {R : Type u_1} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] (h : ringKrullDim R ≠ 0) : maximalIdeal R ^ 2 < maximalIdeal R

In a Noetherian local ring of positive Krull dimension, the square of the maximal ideal is strictly contained in the maximal ideal.

@[deprecated "Use `IsLocalRing.maximalIdeal_sq_lt_of_ringKrullDim_ne_zero` instead" (since := "2026-05-13")]

theorem IsLocalRing.maximalIdeal_sq_lt {R : Type u_1} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] (h : 0 < ringKrullDim R) : maximalIdeal R ^ 2 < maximalIdeal R