krullDim_ne_bot_of_finiteDimensionalOrder

Mathlib.Order.KrullDimension

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

← MathLib Explorer

English

If α is finite-dimensional, then krullDim α ≠ ⊥.

Русский

Если α конечномерна, то размерность Крull не равна нижнему пределу.

LaTeX

$$$\operatorname{krullDim}(\alpha) \neq ⊥$$$

Lean4

theorem krullDim_ne_bot_of_finiteDimensionalOrder [FiniteDimensionalOrder α] : krullDim α ≠ ⊥ :=
  (finiteDimensionalOrder_iff_krullDim_ne_bot_and_top.mp ‹_›).1

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

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

Разделы

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

Аффилиация

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