maximalIdeal_height_eq_ringKrullDim

English

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

Русский

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

LaTeX

$$$\operatorname{height}(\text{IsLocalRing.maximalIdeal } R) = \operatorname{ringKrullDim} R.$$$

Lean4

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

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