Hilbert basis theorem

I remember learning this theorem early 2015, but I could not remember its proof at all. Today, I relearned it. It employed a beautiful induction argument to transfer the Noetherianness (in the form of finite generation) from R to R[x] via the leading coefficient.

Hilbert Basis TheoremIf R is a Noetherian ring, then so is R[x].

Proof: Take some ideal J in R. Notice that if we partition J by degree, we get from the leading coefficients appearing in each an ascending chain (that has to become constant eventually, say at k). Take finite sets A_n \subset J for m \leq n \leq k, where m is the smallest possible non-zero degree such that the I_ns for the leading coefficient ideals are generated. With this we can for any polynomial p construct a finite combination within A = \displaystyle\cup_{n=m}^k A_n that equates to p leading coefficient wise, and thereby subtraction reduces to a lower degree. Such naturally lends itself induction, with m as the base case. For m any lower degree polynomial is the zero polynomial. Now assume, as the inductive hypothesis that A acts as a finite generating set all polynomials with degree at most n. If n+1 \leq k, we can cancel out the leading coefficient using our generating set, and then use the inductive hypothesis. If n+1 > k, we can by our inductive hypothesis generate with A a degree n polynomial with same leading coefficient (and thereby a degree n+1 one multiplying by x) and from that apply our inductive hypothesis again, this time on our difference.