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 to via the leading coefficient.
Hilbert Basis Theorem: If is a Noetherian ring, then so is .
Proof: Take some ideal in . Notice that if we partition by degree, we get from the leading coefficients appearing in each an ascending chain (that has to become constant eventually, say at ). Take finite sets for , where is the smallest possible non-zero degree such that the s for the leading coefficient ideals are generated. With this we can for any polynomial construct a finite combination within that equates to leading coefficient wise, and thereby subtraction reduces to a lower degree. Such naturally lends itself induction, with as the base case. For any lower degree polynomial is the zero polynomial. Now assume, as the inductive hypothesis that acts as a finite generating set all polynomials with degree at most . If , we can cancel out the leading coefficient using our generating set, and then use the inductive hypothesis. If , we can by our inductive hypothesis generate with a degree polynomial with same leading coefficient (and thereby a degree one multiplying by ) and from that apply our inductive hypothesis again, this time on our difference.