Divisor-class criterion for unique factorization (source code)

= Divisor-class criterion for unique factorization
{title2=$\operatorname{Cl}(A)=0$}

A <Noetherian ring> that is an <integrally closed domain> is a <unique factorization domain> exactly when its <divisor class group> vanishes. Indeed, vanishing says every <prime Weil divisor>, equivalently every height-one prime ideal, is principal.