primeHeight_ne_top

Mathlib.RingTheory.Ideal.Height

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

← MathLib Explorer

English

For a prime ideal I, I.primeHeight ≠ ⊤.

Русский

Для простого идеала I, primeHeight(I) ≠ ⊤.

LaTeX

$$I.primeHeight ≠ ⊤$$

Lean4

theorem primeHeight_ne_top (I : Ideal R) [I.FiniteHeight] [I.IsPrime] : I.primeHeight ≠ ⊤ :=
  by
  rw [← I.height_eq_primeHeight]
  exact Ideal.height_ne_top ‹I.IsPrime›.ne_top

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

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

Разделы

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

Аффилиация

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