If $R$ is a Noetherian ring then $R[[x]]$ is also Noetherian

Let $R$ be a Noetherian ring. How can one prove that the ring of the formal power series $R[[x]]$ is again a Noetherian ring?

It is well-known that the ring of polynomials $R[x]$ is Noetherian. I try imitating the standard proof of the fact by replacing "leading coefficients" by "lowest coefficients", but it does not work.

Solution 1:

Step 1: Let $f\in R[[x]]$ such that the constant term of $f$ is a unit. Then $f$ is a unit. It's an easy exercise to construct $f^{-1}$ term-by-term.

Step 2: Show that if $I$ is an ideal, the set of coefficients of lowest nonzero terms of elements of $I$ is an ideal of $R$.

Step 3: Consider an ascending chain of ideal. $I_1\subset I_2\subset\ldots$, and let $J_1\subset J_2\subset\ldots$ be the corresponding chain of ideals in $R$, where $J_i$ is the ideal of coefficients of lowest nonzero terms of elements of $I_i$.

Step 4: $J_1\subset J_2\subset\ldots$ can only be strict inclusion at finitely many places. The only other way to have strict inclusion in $I_1\subset I_2\subset\ldots$ is via the lowest degree in $x$ of nonzero terms, which can only decrease finitely many times.

Solution 2:

Hilbert's basis theorem can be adapted for formal power series. I found a .pdf on the internet that describes the process well, if you look at section 8.2.3: here.

Basically, you simply replace the degree of the polynomial with the lowest degree in the power series.