height_le_spanRank

Mathlib.RingTheory.Ideal.KrullsHeightTheorem

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

← MathLib Explorer

English

For a proper ideal I in a Noetherian ring, height(I) ≤ spanRank(I).

Русский

Для пригодного идеала I в кольце Ноetherian высота I не превосходит spanRank(I).

LaTeX

$$$I.height \le I.spanRank$$$

Lean4

theorem height_le_spanRank (I : Ideal R) (hI : I ≠ ⊤) : I.height ≤ I.spanRank :=
  by
  trans ↑I.spanRank.toENat
  · exact_mod_cast I.height_le_spanRank_toENat hI
  · exact I.spanRank.ofENat_toENat_le

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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