instKrullDimLEOfNatNat

Mathlib.RingTheory.Spectrum.Prime.Noetherian

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

English

If R is Artinian, then Krull dimension of R is at most 0.

Русский

Если R Artinian, то размер Крулля R не превосходит 0.

LaTeX

$$$\\mathrm{KrullDim}(R) \\le 0$ (for Artinian~R)$$

Lean4

instance : Ring.KrullDimLE 0 R :=
  .mk₀ fun _ _ ↦ inferInstance

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

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

Разделы

Аффилиация

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