exists_mul_mem_of_mem_minimalPrimes

English

If p ∈ I.minimalPrimes and x ∈ p, there exists y with y ∉ I and xy ∈ I.

Русский

Пусть p ∈ I.minimalPrimes и x ∈ p; существует y ∉ I, такое что xy ∈ I.

LaTeX

$$$p \in I.minimalPrimes \Rightarrow (\forall x \in p)(\exists y \notin I, \; x y \in I)$$$

Lean4

theorem exists_mul_mem_of_mem_minimalPrimes {p : Ideal R} (hp : p ∈ I.minimalPrimes) {x : R} (hx : x ∈ p) :
    ∃ y ∉ I, x * y ∈ I := by
  classical
  obtain ⟨y, hy, n, hx⟩ := Ideal.iUnion_minimalPrimes.subset (Set.mem_biUnion hp hx)
  have H : ∃ m, x ^ m * y ^ n ∈ I := ⟨n, mul_pow x y n ▸ hx⟩
  have : Nat.find H ≠ 0 := fun h ↦ hy ⟨n, by simpa only [h, pow_zero, one_mul] using Nat.find_spec H⟩
  refine ⟨x ^ (Nat.find H - 1) * y ^ n, Nat.find_min H (Nat.sub_one_lt this), ?_⟩
  rw [← mul_assoc, ← pow_succ', tsub_add_cancel_of_le (Nat.one_le_iff_ne_zero.mpr this)]
  exact Nat.find_spec H

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