Theorems · Theorem · order theory

Order.krullDim_eq_iSup_coheight

∀ {α : Type u_1} [inst : Preorder α], Order.krullDim α = ⨆ a, ↑(Order.coheight a)

The Krull dimension is the supremum of the elements' coheights. If α is Nonempty, then krullDim_eq_iSup_coheight_of_nonempty, with the coercion from ℕ∞ to WithBot ℕ∞ outside the supremum, can be more convenient.

Defined in

Mathlib.Order.KrullDimension

Cited by

1 results in Mathlib

Foundations

Depth 61 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Preorder