mem_minimalPrimes_of_primeHeight_eq_height

English

If J is prime with height equal to I.height, then J belongs to minimalPrimes(I).

Русский

Если J простый и height(J) = height(I), то J принадлежит минимальным-primes(I).

LaTeX

$$$J \text{ prime},\ J.height = I.height \Rightarrow J \in I.minimalPrimes.$$$

Lean4

theorem mem_minimalPrimes_of_primeHeight_eq_height {I J : Ideal R} [J.IsPrime] (e : I ≤ J)
    (e' : J.primeHeight = I.height) [J.FiniteHeight] : J ∈ I.minimalPrimes :=
  by
  rw [← J.height_eq_primeHeight] at e'
  exact mem_minimalPrimes_of_height_eq e (e' ▸ le_refl _)

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