ringKrullDim

Mathlib.RingTheory.KrullDimension.Basic

URI: https://scilib.ai/kg/mathlib#ringKrullDim

← MathLib Explorer

English

If R has finite ring Krull dimension, then ringKrullDim R < ⊤.

Русский

Если размерность Р конечна, то ringKrullDim R меньше верхнего элемента.

LaTeX

$$$ringKrullDim R < \\top$$$

Lean4

/-- The ring-theoretic Krull dimension is the Krull dimension of its spectrum ordered by inclusion.
-/
noncomputable def ringKrullDim (R : Type*) [CommSemiring R] : WithBot ℕ∞ :=
  krullDim (PrimeSpectrum R)

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

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

Разделы

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

Аффилиация

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