Bounded-degree coefficient proof of Hilbert basis theorem (source code)

= Bounded-degree coefficient proof of Hilbert basis theorem

For an <ideal> $I$ in $R[x]$, let $J_n$ contain the coefficients of $x^n$ in its elements of degree at most $n$. These are <ideals> of $R$ and form an ascending chain, since multiplying by $x$ embeds one into the next. If $R$ is a <Noetherian ring>, the chain stabilizes at $N$, and each $J_n$ for $0\le n\le N$ has finitely many generators. Choose corresponding polynomials in $I$. Their union generates $I$: for an element of degree $d$, subtract a combination of the chosen polynomials for $J_d$ if $d<N$, or the polynomials for $J_N$ multiplied by $x^{d-N}$ otherwise. This cancels its leading coefficient and lowers its degree. Induction completes the proof without assuming that $R$ is an <integral domain>.