Gauss lemma: primitive factorisations over $\mathbb{Q}$ can be cleared to primitive factorisations over $\mathbb{Z}$

By [L2], choose an integer numerator and nonzero integer denominator for each of the finitely many coefficients of $g$ and $h$. Their denominator products are nonzero by [L4] and are common denominators, so [L3] and division by the positive contents of the cleared polynomials give $g=rG$ and $h=sH$ with $r,s\in {\mathbb{Q}}^{\times }$ and primitive $G,H\in \mathbb{Z}[x]$ of the same positive degrees as $g,h$.

The equality $f=rsGH$, after writing $rs=a\mathrm{/}b$ in lowest terms with $b>0$, gives $bf=aGH$; [L1] makes both $f$ and $GH$ primitive, so content multiplicativity gives $b=\mathrm{\mid }a\mathrm{\mid }$ and therefore $a\mathrm{/}b=\pm 1$; hence $f=\pm GH$.

Any integer factorization of a primitive polynomial into two nonunits has both factors of positive degree: a nonunit constant factor would have content greater than $1$, contradicting [L1]. Conversely, steps 1.1 and 2.1 turn every rational positive-degree factorization into an integer one. By [L5], irreducibility over the two rings is therefore equivalent for primitive positive-degree polynomials.