Noetherianity of formal power series rings ($R\text{ Noetherian}⟹R[[X]]\text{ Noetherian}$)

For a commutative Noetherian ring, the ideals of lowest possible coefficients of an ideal in $R[[X]]$ form an ascending chain. Choose lifts of finite generating sets through the stabilization degree. Successive coefficient cancellation expresses any series in the ideal using these finitely many lifts. The multiplier series converge coefficientwise, so this generates the actual ideal without first assuming it is closed. Iterating gives the result for finitely many variables.