height_mono — Mathlib

English

If I ≤ J are ideals, then I.height ≤ J.height.

Русский

Если I ⊆ J, то height(I) ≤ height(J).

LaTeX

$$I ≤ J → I.height ≤ J.height$$

Lean4

@[gcongr]
theorem height_mono {I J : Ideal R} (h : I ≤ J) : I.height ≤ J.height :=
  by
  simp only [height]
  refine le_iInf₂ (fun p hp ↦ ?_)
  have := Ideal.minimalPrimes_isPrime hp
  obtain ⟨q, hq, e⟩ := Ideal.exists_minimalPrimes_le (h.trans hp.1.2)
  haveI := Ideal.minimalPrimes_isPrime hq
  exact (iInf₂_le q hq).trans (Ideal.primeHeight_mono e)

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