ringKrullDim_nonneg_of_nontrivial

Mathlib.RingTheory.KrullDimension.Basic

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

English

If R is nontrivial, then ringKrullDim R ≥ 0.

Русский

Если R не тривиально, тогда ringKrullDim R не меньше нуля.

LaTeX

$$$0 \\le ringKrullDim R$$$

Lean4

theorem ringKrullDim_nonneg_of_nontrivial [Nontrivial R] : 0 ≤ ringKrullDim R :=
  krullDim_nonneg

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

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

Разделы

Аффилиация

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