finiteHeight_of_finiteRingKrullDim

English

If R has finite Krull dimension, then every ideal I has finite height.

Русский

Если у кольца R конечна размерность Крull, тогда для любого идеала I высота I конечна.

LaTeX

$$$\forall I \; \operatorname{FiniteHeight}(I).$$$

Lean4

instance (priority := 900) finiteHeight_of_finiteRingKrullDim {I : Ideal R} [FiniteRingKrullDim R] : I.FiniteHeight :=
  by
  rw [finiteHeight_iff, or_iff_not_imp_left, ← lt_top_iff_ne_top, ← WithBot.coe_lt_coe]
  intro h
  have h1 := ringKrullDim_lt_top (R := R)
  have h2 := Ideal.height_le_ringKrullDim_of_ne_top h
  exact lt_of_le_of_lt h2 h1

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