height_lt_top

Mathlib.RingTheory.Ideal.Height

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

English

If I ≠ ⊤ and FiniteHeight, then I.height < ⊤.

Русский

Если I ≠ ⊤ и FiniteHeight, то height(I) < ⊤.

LaTeX

$$(I ≠ ⊤) ∧ [I.FiniteHeight] → I.height < ⊤$$

Lean4

theorem height_lt_top {I : Ideal R} (hI : I ≠ ⊤) [I.FiniteHeight] : I.height < ⊤ :=
  (Ideal.height_ne_top hI).lt_top

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

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

Разделы

Аффилиация

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