maximalIdeal_primeHeight_eq_ringKrullDim

English

In a local ring, the primeHeight of the maximal ideal equals the Krull dimension of the ring.

Русский

В локальном кольце простая высота максимального идеала равна размерности Крull кольца.

LaTeX

$$$\text{In a local ring } R, \ (\text{IsLocalRing.maximalIdeal } R).primeHeight = \operatorname{ringKrullDim} R.$$$

Lean4

/-- The prime height of the maximal ideal equals the Krull dimension in a local ring -/
@[simp]
theorem maximalIdeal_primeHeight_eq_ringKrullDim [IsLocalRing R] :
    (IsLocalRing.maximalIdeal R).primeHeight = ringKrullDim R :=
  by
  rw [ringKrullDim, Ideal.primeHeight, ← Order.height_top_eq_krullDim]
  rfl

Похожие утверждения