krullDim_of_isSimpleOrder

Mathlib.Order.KrullDimension

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

← MathLib Explorer

English

If α is a simple order, then krullDim α = 1.

Русский

Если α — простой порядок, тогда krullDim α = 1.

LaTeX

$$@theorem krullDim_of_isSimpleOrder {α} [PartialOrder α] [BoundedOrder α] [IsSimpleOrder α] : krullDim α = 1$$

Lean4

@[simp]
theorem krullDim_of_isSimpleOrder {α : Type*} [PartialOrder α] [BoundedOrder α] [IsSimpleOrder α] : krullDim α = 1 :=
  krullDim_eq_one_iff_of_boundedOrder.mpr ‹_›

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

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

Разделы

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

Аффилиация

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