Noetherianity of a formal power series ring

A formal power series ring $R[[x]]$ is Noetherian if and only if $R$ is Noetherian. In the forward direction, use the quotient ring $R[[x]]/(x)\cong R$. In the reverse direction, for an ideal $I$ consider the ascending sequence of ideals of $R$ formed by the coefficient of $x^n$ in $I\cap x^{n}R[[x]]$. Stabilization and finite generation give a finite list of series that generate $I$ by successive coefficient cancellation.

For an ideal $H\subseteq R[[X]]$, let $A_n$ consist of coefficients of $X^n$ in members of $H$ with all lower coefficients zero. These are ideals of $R$ and $A_n\subseteq A_{n+1}$, by multiplication by $X$. If $R$ is Noetherian, this chain stabilizes. Choose series whose leading coefficients generate the finitely many distinct coefficient ideals, then cancel coefficients successively. The accumulated multipliers are formal power series, giving an ordinary finite ideal generating set for $H$, rather than merely a dense subideal.