finiteHeight_iff_lt

Mathlib.RingTheory.Ideal.Height

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

English

For a given ideal I, FiniteHeight is equivalent to either I = ⊤ or height(I) < ∞.

Русский

Для идеала I равносильно: либо I = ⊤, либо height(I) < ∞.

LaTeX

$$$\text{Ideal.FiniteHeight } I \iff I = \top \lor I.height < \top$$$

Lean4

theorem finiteHeight_iff_lt {I : Ideal R} : Ideal.FiniteHeight I ↔ I = ⊤ ∨ I.height < ⊤ := by
  rw [Ideal.finiteHeight_iff, lt_top_iff_ne_top]

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

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

Разделы

Аффилиация

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