coheight_bot_eq_krullDim — Mathlib

English

If α has a bottom element, then the coheight of the bottom equals the Krull dimension of α.

Русский

Если у множества α есть нижняя граница, то ко-высота нуля равна размерности Крull α.

LaTeX

$$$\operatorname{coheight}(\bot) = \operatorname{krullDim}(\alpha)$$$

Lean4

@[simp] -- not as useful as a simp lemma as it looks, due to the coe on the left

theorem coheight_bot_eq_krullDim [OrderBot α] : coheight (⊥ : α) = krullDim α :=
  by
  rw [← krullDim_orderDual]
  exact height_top_eq_krullDim (α := αᵒᵈ)

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