Minimal-prime criterion for a Noetherian unique factorization domain (source code)

= Minimal-prime criterion for a Noetherian unique factorization domain
{c}

A Noetherian integral domain is a unique factorization domain exactly when every prime ideal minimal among the nonzero prime ideals is principal. The converse uses the Krull principal ideal theorem to prove that every irreducible element generates a prime ideal.