Kaplansky criterion for factoriality

We prove Kaplansky criterion for factoriality: an integral domain is a UFD if and only if every nonzero prime ideal contains a prime element.

Main declarations

iff_exists_prime_mem_of_isPrime: an integral domain is a UFD if and only if every nonzero prime ideal contains a prime element.

theorem UniqueFactorizationMonoid.iff_exists_prime_mem_of_isPrime {R : Type u_1} [CommSemiring R] [IsDomain R] : UniqueFactorizationMonoid R ↔ ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x

Kaplansky's criterion: an integral domain is a UFD if and only if every nonzero prime ideal contains a prime element.