primeHeight_strict_mono — Mathlib

English

If I < J are prime ideals and J has finite height, then I.primeHeight < J.primeHeight.

Русский

Если I < J простые идеалы и height(J) конечна, то I.primeHeight < J.primeHeight.

LaTeX

$$[I.IsPrime] [J.IsPrime] (h : I < J) [J.FiniteHeight] : I.primeHeight < J.primeHeight$$

Lean4

@[gcongr]
theorem primeHeight_strict_mono {I J : Ideal R} [I.IsPrime] [J.IsPrime] (h : I < J) [J.FiniteHeight] :
    I.primeHeight < J.primeHeight := by
  rw [primeHeight]
  have : I.FiniteHeight :=
    by
    rw [Ideal.finiteHeight_iff, ← lt_top_iff_ne_top, Ideal.height_eq_primeHeight]
    right
    exact lt_of_le_of_lt (Ideal.primeHeight_mono h.le) (Ideal.primeHeight_lt_top J)
  exact Order.height_strictMono h (Ideal.primeHeight_lt_top _)

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