Solution (source code)

= Solution

A nonzero <primitive polynomial> in $\mathbb Z[x]$ has greatest common divisor of its coefficients equal to one. Suppose primitive polynomials $f,g$ had a product whose coefficients were all divisible by some prime $p$. Their reductions in $\mathbb F_p[x]$ are both nonzero, because neither polynomial has every coefficient divisible by $p$. A polynomial ring over a field is an <integral domain>, so their product is nonzero modulo $p$, a contradiction. Hence \b[the product of primitive polynomials is primitive].

To deduce unique factorization, write any nonzero integer polynomial as its positive <polynomial content> times a primitive polynomial, with its sign treated as a unit. The preceding result gives multiplicativity of content. Factor the primitive part over the Euclidean polynomial ring $\mathbb Q[x]$, and rescale every irreducible rational factor to a primitive integer polynomial. If $f=q\prod_if_i$ with all polynomials primitive and $q=a/b$ in lowest terms, the equality $bf=a\prod_if_i$ has contents $b$ and $|a|$. Thus $b=|a|$, forcing $q=\pm1$. The rational factorization therefore lifts to an integer factorization.

A primitive integer polynomial is irreducible over $\mathbb Z$ exactly when it is irreducible over $\mathbb Q$: an integer factorization gives a rational one, and a rational factorization lifts by the same primitive-content argument. Factor the content into integer primes. Existence and uniqueness over the integers and over $\mathbb Q[x]$ now give existence and uniqueness of the resulting factorization into constant prime factors and primitive irreducible polynomial factors, up to order and signs. Therefore $\boxed{\mathbb Z[x]\text{ is a unique factorization domain}}$. This is the full lifting step in <Gauss lemma for polynomials>.