coheight_eq_krullDim_Ici — Mathlib

English

For every x in α, the coheight of x equals the Krull dimension of the subposet {y in α | x ≤ y}.

Русский

Для каждого x в α ко-высота x равна размерности Крull подмножества {y | x ≤ y}.

LaTeX

$$$\operatorname{coheight}(x) = \operatorname{krullDim}(\{ y \in α : x \le y \})$$$

Lean4

theorem coheight_eq_krullDim_Ici {α : Type*} [Preorder α] (x : α) : (coheight x : ℕ∞) = krullDim (Set.Ici x) :=
  by
  rw [coheight, ← krullDim_orderDual, Order.krullDim_eq_of_orderIso (OrderIso.refl _)]
  exact height_eq_krullDim_Iic _

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