coheight_eq_zero

Mathlib.Order.KrullDimension

URI: https://scilib.ai/kg/mathlib#Order.coheight_eq_zero

← MathLib Explorer

English

The elements of coheight zero are exactly the maximal elements.

Русский

Элементы коheight равные нулю — именно максимальные элементы.

LaTeX

$$coheight x = 0 \iff IsMax x$$

Lean4

/-- The elements of coheight zero are the maximal elements. -/
@[simp]
theorem coheight_eq_zero {x : α} : coheight x = 0 ↔ IsMax x :=
  height_eq_zero (α := αᵒᵈ)

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru