_example

Mathlib.RingTheory.KrullDimension.Zero

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

English

In a local ring of Krull dimension zero, there exists a unique prime ideal.

Русский

В локальном кольце нулевой размерности существует единственный простой идеал.

LaTeX

$$$\\exists! I:\\Ideal R, I.IsPrime$$$

Lean4

/-- Note that the `ringKrullDim` of the trivial ring is `⊥` and not `0`. -/
example [Subsingleton R] : Ring.KrullDimLE 0 R :=
  inferInstance

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

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

Разделы

Аффилиация

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