Hilbert basis theorem: if $R$ is Noetherian then $R[x]$ is Noetherian

Given: A Noetherian commutative ring $R$ and its polynomial ring $R[x]$.

For every commutative ring $R$, the coefficientwise addition and convolution multiplication make $R[x]$ a commutative ring, and the constant-polynomial map $R\to R[x]$ is an injective unital ring homomorphism (Polynomial convolution makes $R[x]$ a commutative ring containing $R$ as its constant subring).

Over a Noetherian commutative ring $R$, every ideal of $R[x]$ is generated by finitely many polynomials realising generators of its stage ideals up to a stabilisation degree; in particular every ideal of $R[x]$ is finitely generated (Over a Noetherian ring, an ideal of $R[x]$ is generated by finitely many polynomials realising generators of its stages up to the stabilisation degree).

A commutative ring whose ideals are all finitely generated is Noetherian. This is the choice-free implication $2\Rightarrow 1$ of A commutative ring is Noetherian exactly when every ideal is finitely generated, exactly when its ideals satisfy the ascending chain condition, and exactly when every nonempty set of ideals has a maximal member, established by the regular-module/ideal identification in its proof steps 1.1–3.1. Its dependent-choice assumption is used only to pass from ACC to the maximal condition; that implication is not used here.