[proofplan] We reduce the problem to two ingredients: existence and uniqueness of factorisation into irreducibles in $R[x]$. For existence, we factor out the content of a polynomial to reduce to primitive polynomials, then use the fact that $F[x]$ is a UFD (where $F = \operatorname{Frac}(R)$) together with [Gauss's Lemma](/theorems/858) to lift irreducible factorisations from $F[x]$ back to $R[x]$. For uniqueness, we again use Gauss's Lemma and uniqueness in $F[x]$ to show that any two irreducible factorisations in $R[x]$ agree up to reordering and multiplication by units. [/proofplan]

[step:Factor out the content and reduce to primitive polynomials]Let $f \in R[x]$ be a nonzero non-unit element. We must show that $f$ admits a factorisation into irreducible elements of $R[x]$. If $\deg(f) = 0$, then $f = a \in R$ is a nonzero non-unit element of $R$. Since $R$ is a UFD, $a$ factors into irreducibles in $R$, and every irreducible element of $R$ remains irreducible in $R[x]$ (an element of $R$ that factors non-trivially in $R[x]$ must factor non-trivially in $R$, since a product of polynomials of positive degree has positive degree). So suppose $\deg(f) \ge 1$. Write $f = c(f) \cdot f^*$, where $c(f) \in R$ is the content of $f$ — the greatest common divisor of the coefficients of $f$, well-defined up to units since $R$ is a UFD — and $f^* \in R[x]$ is the primitive part, satisfying $c(f^*) \sim 1_R$ (i.e., the content of $f^*$ is a unit). If $c(f)$ is not a unit, factor $c(f)$ into irreducibles in $R$, which are also irreducible in $R[x]$ as argued above. It remains to factor the primitive polynomial $f^*$.[/step]

[guided]Let $f \in R[x]$ be a nonzero non-unit. We first handle the base case $\deg(f) = 0$. If $f = a \in R$ is a nonzero non-unit, then since $R$ is a UFD, $a$ admits a factorisation $a = p_1 \cdots p_m$ into irreducible elements of $R$. Each $p_i$ remains irreducible in $R[x]$: if $p_i = g \cdot h$ in $R[x]$ with $g, h$ non-units, then $0 = \deg(p_i) = \deg(g) + \deg(h)$ forces $\deg(g) = \deg(h) = 0$, so $g, h \in R$, contradicting the irreducibility of $p_i$ in $R$. This settles the constant case. Now suppose $\deg(f) \ge 1$. The content of $f = a_n x^n + \dots + a_0 \in R[x]$ is $c(f) = \gcd(a_n, \dots, a_0)$, computed in the UFD $R$ and well-defined up to multiplication by units of $R$. We write $f = c(f) \cdot f^*$ where the primitive part $f^* = f / c(f) \in R[x]$ satisfies $c(f^*) \sim 1_R$. Why does this decomposition reduce the problem? The content is multiplicative: for any $g, h \in R[x]$, we have $c(gh) \sim c(g) \cdot c(h)$. This classical fact means that a product of primitive polynomials is primitive. Consequently, when factoring $f = c(f) \cdot f^*$, the constant part and the polynomial part decouple — we factor $c(f)$ into irreducibles in $R$ (which are irreducible in $R[x]$ by the degree argument above) and then factor the primitive polynomial $f^*$ separately. If $c(f)$ is a unit, there is nothing to factor in $R$ and we proceed directly to factoring $f^*$. If $c(f)$ is a non-unit, we apply the UFD property of $R$ to write $c(f) = p_1 \cdots p_m$ with each $p_i$ irreducible in $R$, hence irreducible in $R[x]$. It remains to show that the primitive polynomial $f^*$ also factors into irreducibles in $R[x]$, which is the content of the next step. Note that the content-primitive decomposition $f = c(f) \cdot f^*$ is essentially unique: if $f = d \cdot g$ with $d \in R$ and $g$ primitive, then $d \sim c(f)$ and $g = f^*$ up to multiplication by a unit of $R$. This uniqueness will be essential in the final step when we prove uniqueness of the full factorisation.[/guided]

[step:Factor a primitive polynomial into irreducibles using $F[x]$] Let $F = \operatorname{Frac}(R)$ denote the field of fractions of $R$. Since $F$ is a field, $F[x]$ is a Euclidean domain and hence a UFD by [Principal Ideal Domains Are Unique Factorization Domains](/theorems/867) (every Euclidean domain is a PID). By [Unique Factorization in the Polynomial Ring over a Field](/theorems/3237), every nonzero polynomial in $F[x]$ factors uniquely into irreducibles. Let $f^* \in R[x]$ be primitive with $\deg(f^*) \ge 1$. We view $f^*$ as an element of $F[x]$ via the inclusion $R[x] \hookrightarrow F[x]$. In $F[x]$, write \begin{align*} f^* = q_1 q_2 \cdots q_s \end{align*} where each $q_j \in F[x]$ is irreducible in $F[x]$. Each $q_j$ has coefficients in $F$, so we may clear denominators: for each $j$, there exist $d_j \in R \setminus \{0\}$ such that $d_j q_j \in R[x]$. Write $d_j q_j = c(d_j q_j) \cdot q_j^*$ where $q_j^* \in R[x]$ is primitive. Since $q_j$ and $q_j^*$ differ by a nonzero scalar in $F$, $q_j^*$ is irreducible in $F[x]$. By [Gauss's Lemma](/theorems/858), since each $q_j^*$ is primitive and irreducible in $F[x]$, each $q_j^*$ is irreducible in $R[x]$. Substituting back: \begin{align*} f^* = q_1 \cdots q_s = \frac{c(d_1 q_1)}{d_1} \cdots \frac{c(d_s q_s)}{d_s} \cdot q_1^* \cdots q_s^*. \end{align*} The product $q_1^* \cdots q_s^*$ is primitive (since the product of primitive polynomials is primitive, by multiplicativity of content). Since $f^*$ is also primitive, comparing contents on both sides gives \begin{align*} c(f^*) \sim \frac{c(d_1 q_1)}{d_1} \cdots \frac{c(d_s q_s)}{d_s} \cdot c(q_1^* \cdots q_s^*). \end{align*} Since $c(f^*) \sim 1_R$ and $c(q_1^* \cdots q_s^*) \sim 1_R$, the scalar prefactor $\prod_j c(d_j q_j)/d_j$ is a unit in $R$. Absorbing this unit into $q_1^*$, we obtain \begin{align*} f^* = u \cdot q_1^* \cdots q_s^* \end{align*} where $u \in R^\times$. Since $u$ is a unit, $u \cdot q_1^*$ is an associate of $q_1^*$ and hence irreducible in $R[x]$. This gives the desired factorisation of $f^*$ into irreducibles in $R[x]$.[/step]

[guided]Let $f^* \in R[x]$ be primitive with $\deg(f^*) \ge 1$. The key idea of this step is to exploit the fact that factorisation is much easier in $F[x]$ (where we have the Euclidean algorithm) and then pull the result back to $R[x]$ using Gauss's Lemma. We view $f^*$ as an element of $F[x]$ via the inclusion $R[x] \hookrightarrow F[x]$, which is well-defined because $R \hookrightarrow F = \operatorname{Frac}(R)$ is an inclusion of rings (every $r \in R$ embeds as $r/1_R \in F$), and this extends coefficient-wise to $R[x] \hookrightarrow F[x]$. Since $F$ is a field, $F[x]$ is a Euclidean domain with the degree function as the Euclidean norm. Every Euclidean domain is a PID, and by [Principal Ideal Domains Are Unique Factorization Domains](/theorems/867), every PID is a UFD. So $f^*$ factors in $F[x]$ as \begin{align*} f^* = q_1 q_2 \cdots q_s \end{align*} where each $q_j \in F[x]$ is irreducible in $F[x]$. Each $q_j$ has coefficients in $F = \operatorname{Frac}(R)$, which means the coefficients are fractions $a/b$ with $a, b \in R$. To bring these polynomials back into $R[x]$, we clear denominators: for each $j$ there exists $d_j \in R \setminus \{0\}$ such that $d_j q_j \in R[x]$ (take $d_j$ to be a common denominator of the coefficients of $q_j$). We then extract the content: write $d_j q_j = c(d_j q_j) \cdot q_j^*$ where $q_j^* \in R[x]$ is primitive. Since $q_j^* = (d_j / c(d_j q_j)) \cdot q_j$ is a nonzero $F$-scalar multiple of $q_j$, and irreducibility in $F[x]$ is preserved under multiplication by nonzero scalars (such a multiplication is a unit operation in $F[x]$), $q_j^*$ is irreducible in $F[x]$. Now we apply [Gauss's Lemma](/theorems/858), which is the crucial bridge between $F[x]$ and $R[x]$. This theorem requires: (i) $R$ is a UFD, which is our hypothesis; (ii) $q_j^*$ is a primitive polynomial in $R[x]$, which holds by construction; (iii) $q_j^*$ is irreducible in $F[x]$, which we just verified. Gauss's Lemma concludes that each $q_j^*$ is irreducible in $R[x]$. Without Gauss's Lemma, we would have no way to transfer irreducibility from $F[x]$ back to $R[x]$: a polynomial can be irreducible over a larger ring but reducible over a smaller one, and Gauss's Lemma rules this out for primitive polynomials. We now need to reconcile the factorisations and show that $f^*$ is a product of the $q_j^*$ up to a unit. Substituting back: \begin{align*} f^* = q_1 \cdots q_s = \frac{c(d_1 q_1)}{d_1} \cdots \frac{c(d_s q_s)}{d_s} \cdot q_1^* \cdots q_s^*. \end{align*} By the multiplicativity of content ($c(gh) \sim c(g) \cdot c(h)$ for all $g, h \in R[x]$), the product $q_1^* \cdots q_s^*$ is primitive since each factor is primitive. Comparing contents on both sides: $c(f^*) \sim \prod_j \frac{c(d_j q_j)}{d_j} \cdot c(q_1^* \cdots q_s^*)$. Since $c(f^*) \sim 1_R$ (the hypothesis that $f^*$ is primitive) and $c(q_1^* \cdots q_s^*) \sim 1_R$ (product of primitives is primitive), the prefactor $\prod_j c(d_j q_j)/d_j$ is a unit $u \in R^\times$. Absorbing $u$ into the first factor, we obtain $f^* = u \cdot q_1^* \cdots q_s^*$. Since $u \in R^\times$, the polynomial $u \cdot q_1^*$ is an associate of $q_1^*$ and hence irreducible in $R[x]$. This gives the desired factorisation of $f^*$ into irreducibles in $R[x]$, completing the existence half of the proof.[/guided]

[step:Prove uniqueness of the factorisation up to reordering and units]Suppose $f \in R[x]$ is a nonzero non-unit with two factorisations into irreducibles: \begin{align*} f = a_1 \cdots a_r \cdot p_1 \cdots p_s = b_1 \cdots b_t \cdot q_1 \cdots q_u, \end{align*} where $a_i, b_j \in R$ are irreducible elements of $R$ (hence of $R[x]$) and $p_k, q_l \in R[x]$ are irreducible polynomials of degree $\ge 1$ (necessarily primitive, since an irreducible polynomial of positive degree in a UFD must be primitive: if $c(p_k)$ were a non-unit, we could write $p_k = c(p_k) \cdot p_k^*$ as a non-trivial factorisation, contradicting irreducibility). **Uniqueness of the constant factors.** Taking contents of both sides and using multiplicativity of content: \begin{align*} c(f) \sim a_1 \cdots a_r \cdot c(p_1 \cdots p_s) \sim a_1 \cdots a_r \end{align*} since each $p_k$ is primitive and the product of primitive polynomials is primitive. Similarly, $c(f) \sim b_1 \cdots b_t$. Since $R$ is a UFD, the factorisation of $c(f)$ in $R$ is unique up to reordering and units. Therefore $r = t$ and, after reordering, $a_i \sim b_i$ for each $i$. **Uniqueness of the polynomial factors.** Dividing both sides by $c(f)$ (which is a nonzero element of $R$, hence a non-zero-divisor), we reduce to \begin{align*} p_1 \cdots p_s = v \cdot q_1 \cdots q_u \end{align*} for some unit $v \in R^\times$. View this equation in $F[x]$. Each $p_k$ is primitive and irreducible in $R[x]$. By [Gauss's Lemma](/theorems/858), each $p_k$ is irreducible in $F[x]$. Similarly, each $q_l$ is irreducible in $F[x]$. Since $F[x]$ is a UFD, uniqueness of factorisation in $F[x]$ gives $s = u$ and, after reordering, $p_k = \alpha_k q_k$ for some $\alpha_k \in F^\times$. Since $p_k$ and $q_k$ are both primitive elements of $R[x]$, we must have $\alpha_k \in R^\times$. Indeed, write $\alpha_k = a/b$ with $a, b \in R \setminus \{0\}$ and $\gcd(a, b) \sim 1_R$. Then $b \cdot p_k = a \cdot q_k$, so $c(b \cdot p_k) = b \cdot c(p_k) \sim b$ and $c(a \cdot q_k) = a \cdot c(q_k) \sim a$. Thus $b \sim a$, giving $\alpha_k \in R^\times$. Therefore $p_k \sim q_k$ in $R[x]$ for each $k$. This establishes uniqueness of the factorisation up to reordering and multiplication by units, completing the proof that $R[x]$ is a UFD.[/step]

[guided]Suppose $f \in R[x]$ is a nonzero non-unit with two factorisations into irreducibles: \begin{align*} f = a_1 \cdots a_r \cdot p_1 \cdots p_s = b_1 \cdots b_t \cdot q_1 \cdots q_u, \end{align*} where $a_i, b_j \in R$ are irreducible in $R$ and $p_k, q_l \in R[x]$ are irreducible polynomials of degree $\ge 1$. We must show that $r = t$, $s = u$, and the factors agree up to reordering and units. **Irreducible polynomials of positive degree are primitive.** We first verify that each $p_k$ is primitive. If $c(p_k)$ were a non-unit $d \in R$, then $p_k = d \cdot (p_k / d)$ would be a non-trivial factorisation in $R[x]$: $d$ is a non-unit, and $p_k / d$ is a non-unit since $\deg(p_k / d) = \deg(p_k) \ge 1$. This contradicts the irreducibility of $p_k$. So $c(p_k) \sim 1_R$ for each $k$, and similarly $c(q_l) \sim 1_R$ for each $l$. **Uniqueness of the constant factors.** By the multiplicativity of content, $c(p_1 \cdots p_s) \sim c(p_1) \cdots c(p_s) \sim 1_R$ (each factor is primitive, so the product is primitive). Taking contents of the full factorisation: $c(f) \sim a_1 \cdots a_r \cdot c(p_1 \cdots p_s) \sim a_1 \cdots a_r$. Similarly, $c(f) \sim b_1 \cdots b_t$. Since $R$ is a UFD, the two factorisations of $c(f)$ into irreducibles in $R$ agree up to reordering and units: $r = t$ and $a_i \sim b_i$ after reindexing. **Uniqueness of the polynomial factors.** Dividing both sides by $c(f)$ (a nonzero element of $R$, hence a non-zero-divisor), we obtain $p_1 \cdots p_s = v \cdot q_1 \cdots q_u$ for some unit $v \in R^\times$. We pass to $F[x]$. By [Gauss's Lemma](/theorems/858), a primitive polynomial in $R[x]$ is irreducible in $R[x]$ if and only if it is irreducible in $F[x]$. Since each $p_k$ is primitive and irreducible in $R[x]$, each $p_k$ is irreducible in $F[x]$. The same reasoning shows each $q_l$ is irreducible in $F[x]$. Since $F[x]$ is a UFD, uniqueness of factorisation in $F[x]$ gives $s = u$ and, after reordering, $p_k = \alpha_k q_k$ for some $\alpha_k \in F^\times$. **The scalars $\alpha_k$ are units of $R$.** Write $\alpha_k = a/b$ with $a, b \in R \setminus \{0\}$ and $\gcd(a, b) \sim 1_R$. Then $b \cdot p_k = a \cdot q_k$ in $R[x]$. Taking contents on both sides: $c(b \cdot p_k) = b \cdot c(p_k) \sim b$ (since $p_k$ is primitive), and $c(a \cdot q_k) = a \cdot c(q_k) \sim a$ (since $q_k$ is primitive). Therefore $b \sim a$. Combined with $\gcd(a, b) \sim 1_R$, this forces both $a$ and $b$ to be units of $R$, so $\alpha_k = a/b \in R^\times$. Therefore $p_k \sim q_k$ in $R[x]$ for each $k$, and the two factorisations agree up to reordering and multiplication by units. This completes the proof that $R[x]$ is a UFD.[/guided]