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.  
 A: If $f\in R[[x]]$, we write $o(f)$ for the degree of the first nonzero term of $f$ and $c(f)$ for the first nonzero coefficient of $f$.  Let $I\subseteq R[[x]]$ be an ideal and let $$I_n=\{c(f):f\in I, o(f)=n\}\cup\{0\}.$$  Then each $I_n$ is an ideal in $R$ and $$I_0\subseteq I_1\subseteq I_2\subseteq\dots.$$  Since $R$ is Noetherian, there is some $N$ such that $I_n=I_N$ for all $n\geq N$.  Also, each $I_n$ is finitely generated.  So we can pick finitely many elements $a_1,\dots,a_m\in I$ which witness finite generating sets of $I_n$ for each $n\leq N$.  Let $J$ be the ideal generated by $a_1,\dots,a_m$.  Then for any $f\in I$, there exists $g\in J$ such that $o(f)=o(g)$ and $c(f)=c(g)$ (if $o(f)\leq N$ this is by definition of $J$, and if $o(f)>N$ this follows from the case $o(f)=N$ by multiplying by $x^{o(f)-N}$ since $I_{o(f)}=I_N$).  In other words, we can match the first nonzero term of any element of $I$ with an element of $J$.
We now iterate this to realize an entire element of $I$ as an element of $J$.  We start with $f=f_0\in I$ and pick $g_0\in J$ such that $o(g_0)=o(f_0)$ and $c(g_0)=c(f_0)$.  Now let $f_1=f_0-g_0$; by our choice of $g_0$ we have $o(f_1)>o(f_0)$.  Choose $g_1$ such that $o(g_1)=o(f_1)$ and $c(g_1)=c(f_1)$, and let $f_2=f_1-g_1$.  Repeating this process, we get a sequence of elements $f_n\in I$ and $g_n\in J$ with $f_{n+1}=f_n-g_n$ and $o(f_n)=o(g_n)\geq n$ for each $n$.  In particular, this implies $f_n\to 0$ in the $x$-adic topology so $\sum_n g_n$ converges to $f$.  Moreover, if we write $g_n=\sum b_{in} a_i$, each coefficient $b_{in}$ is divisible by $x^{n-N}$ since $o(a_i)\leq N$ for each $i$ and $o(g_n)\geq n$.  It follows that $\sum_n b_{in}$ converges for each $i$ and we can write $f=\sum g_n=\sum_i(\sum_n b_{in})a_i$.   Thus $f\in J$.  Since $f\in I$ was arbitrary, this means $I=J$ so $I$ is finitely generated.
A: 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.
A: 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. 
A: This also follows from the general fact that if $R$ is a Noetherian commutative ring, then its $I$-adic completion $\widehat{R}$ is Noetherian as well. $R[[x_1,\dots,x_n]]$ is the completion of $R[x_1,\dots,x_n]$ in the $(x_1,\dots,x_n)$-adic topology so it is Noetherian.
