height_strict_mono_of_is_prime — Mathlib

English

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

Русский

Если I < J простые и у J конечна высота, то I.height < J.height.

LaTeX

$$I < J [I.IsPrime] [J.IsPrime] [J.FiniteHeight] : I.height < J.height$$

Lean4

@[gcongr]
theorem height_strict_mono_of_is_prime {I J : Ideal R} [I.IsPrime] (h : I < J) [I.FiniteHeight] : I.height < J.height :=
  by
  rw [Ideal.height_eq_primeHeight I]
  by_cases hJ : J = ⊤
  · rw [hJ, height_top]
    exact I.primeHeight_lt_top
  · rw [← ENat.add_one_le_iff I.primeHeight_ne_top, Ideal.height]
    refine le_iInf₂ (fun K hK ↦ ?_)
    haveI := Ideal.minimalPrimes_isPrime hK
    have : I < K := lt_of_lt_of_le h hK.1.2
    exact Ideal.primeHeight_add_one_le_of_lt this

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