English
Every nonzero prime ideal in a unique factorization domain contains a prime element.
Русский
Любая ненулевая простая идеал в области уникализации содержит простую элемент.
LaTeX
$$$\\exists x \\in I,\\ Prime\\ x$$$
Lean4
/-- Every non-zero prime ideal in a unique factorization domain contains a prime element. -/
theorem exists_mem_prime_of_ne_bot {R : Type*} [CommSemiring R] [IsDomain R] [UniqueFactorizationMonoid R] {I : Ideal R}
(hI₂ : I.IsPrime) (hI : I ≠ ⊥) : ∃ x ∈ I, Prime x := by
classical
obtain ⟨a : R, ha₁ : a ∈ I, ha₂ : a ≠ 0⟩ := Submodule.exists_mem_ne_zero_of_ne_bot hI
replace ha₁ : (factors a).prod ∈ I :=
by
obtain ⟨u : Rˣ, hu : (factors a).prod * u = a⟩ := factors_prod ha₂
rwa [← hu, mul_unit_mem_iff_mem _ u.isUnit] at ha₁
obtain ⟨p : R, hp₁ : p ∈ factors a, hp₂ : p ∈ I⟩ := (hI₂.multiset_prod_mem_iff_exists_mem <| factors a).1 ha₁
exact ⟨p, hp₂, prime_of_factor p hp₁⟩
