Hilbert basis theorem

Hilbert basis theorem: Let $R$ be a commutative ring . If $R$ is Noetherian (i.e. every ascending chain of ideals stabilizes), then the polynomial ring $R[x]$ is Noetherian. More generally, $R[x_1,\dots,x_n]$ is Noetherian for every $n\ge 1$.

Proof sketch: Let $I\triangleleft R[x]$. Consider the ideal $J\subseteq R$ generated by leading coefficients of polynomials in $I$. Noetherianness of $R$ gives finite generators of $J$, and one then uses a degree-reduction argument to show that finitely many polynomials in $I$ generate all of $I$.