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.