ringKrullDim_eq_zero_of_field

Mathlib.RingTheory.KrullDimension.Field

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

English

The Krull dimension of a field is zero.

Русский

Крull размерность поля равна нулю.

LaTeX

$$$\operatorname{ringKrullDim}(F) = 0$ for any field F.$$

Lean4

@[simp]
theorem ringKrullDim_eq_zero_of_field (F : Type*) [Field F] : ringKrullDim F = 0 :=
  krullDim_eq_zero_of_unique

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

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

Разделы

Аффилиация

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