height_le_krullDim

Mathlib.Order.KrullDimension

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

← MathLib Explorer

English

For every a in α, height(a) ≤ krullDim α.

Русский

Для каждого a ∈ α высота(a) ≤ krullDim α.

LaTeX

$$height(\,a\,) \le krullDim(\alpha)$$

Lean4

theorem height_le_krullDim (a : α) : height a ≤ krullDim α :=
  by
  have : Nonempty α := ⟨a⟩
  rw [krullDim_eq_iSup_length]
  simp only [WithBot.coe_le_coe]
  exact height_le fun p _ ↦ le_iSup_of_le p le_rfl

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

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

Разделы

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

Аффилиация

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