Noetherianity of formal power series rings (source code)

= Noetherianity of formal power series rings
{c}
{title2=$R\text{ Noetherian}\implies 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.