primeHeight_le_ringKrullDim

Mathlib.RingTheory.Ideal.Height

URI: https://scilib.ai/kg/mathlib#Ideal.primeHeight_le_ringKrullDim

English

For a prime ideal I, I.primeHeight ≤ ringKrullDim R.

Русский

Для простого идеала I имеет место I.primeHeight ≤ ringKrullDim R.

LaTeX

$$$I.IsPrime \Rightarrow I.primeHeight ≤ \mathrm{ringKrullDim}(R)$$$

Lean4

theorem primeHeight_le_ringKrullDim {I : Ideal R} [I.IsPrime] : I.primeHeight ≤ ringKrullDim R :=
  Order.height_le_krullDim _

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

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

Разделы

Аффилиация

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