krullDim_of_noMaxOrder

Mathlib.Order.KrullDimension

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

English

For any nonempty α with NoMaxOrder, krullDim α = ⊤.

Русский

Для любого непустого α с NoMaxOrder размерность Крull равна ⊤.

LaTeX

$$$\forall α\ [Nonempty(α) \land NoMaxOrder(α)]: \operatorname{krullDim}(\alpha) = \top$$$

Lean4

@[simp]
theorem krullDim_of_noMaxOrder [Nonempty α] [NoMaxOrder α] : krullDim α = ⊤ := by
  simp [krullDim_eq_iSup_coheight, coheight_of_noMaxOrder]

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

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

Разделы

Аффилиация

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