@[reducible, inline]

abbrev IsRegularLocalRing181 (R : Type u_1) [CommRing R] [IsLocalRing R] [IsNoetherianRing R] : Prop

(Definition 18.1) A Noetherian local ring $R$ is regular if its maximal ideal can be generated by $\dim R$ elements (equivalently, $\dim_{R/\mathfrak{m}} \mathfrak{m}/\mathfrak{m}^2 = \dim R$).

theorem ValuationSubring.ringKrullDim_eq_coheight {K : Type u_1} [Field K] (R : ValuationSubring K) : ringKrullDim ↥R = ↑(Order.coheight R)

For a valuation subring $R$ of a field $K$, the ring-theoretic Krull dimension of $R$ equals the order-theoretic coheight of $R$ in the lattice of valuation subrings of $K$.

theorem ValuationSubring.ringKrullDim_add_one_le_of_lt {K : Type u_1} [Field K] {R₁ R₂ : ValuationSubring K} (h : R₁ < R₂) : ringKrullDim ↥R₂ + 1 ≤ ringKrullDim ↥R₁

If $R_1 \subsetneq R_2$ is a strict inclusion of valuation subrings of $K$, then $\dim R_1 \geq \dim R_2 + 1$ (a strictly larger valuation ring has strictly smaller Krull dimension).

theorem nakayama_lemma_18_3 {R : Type u_2} {M : Type u_3} [CommRing R] [IsLocalRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] (h : IsLocalRing.maximalIdeal R • ⊤ = ⊤) : Subsingleton M

(Nakayama's Lemma, 18.3) For a finitely generated module $M$ over a local ring $(R, \mathfrak{m})$, if $\mathfrak{m} M = M$, then $M = 0$.