classical
constructor
intro _ _ hI hI₂
exact Ideal.IsPrime.exists_mem_prime_of_ne_bot hI₂ hI
intro H
exact uniqueFactorizationMonoid_of_exists_prime H hP
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
hP : Set.Nonempty {r | Prime r}
⊢ UniqueFactorizationMonoid R ↔ ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
no goals