instKrullDimLEOfNatNat

Mathlib.RingTheory.KrullDimension.Basic

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

English

If ring Krull dimension is 0 for R, then Ring.KrullDimLE 1 R holds as an instance.

Русский

Если для кольца R выполняется KrullDimLE 0, то Ring.KrullDimLE 1 R следует как экземпляр.

LaTeX

$$$[\mathrm{Ring.KrullDimLE}\;0\;R] \Rightarrow \mathrm{Ring.KrullDimLE}\;1\;R$$$

Lean4

instance [Ring.KrullDimLE 0 R] : Ring.KrullDimLE 1 R :=
  .mono zero_le_one _

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

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

Разделы

Аффилиация

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