Noetherianity of formal power series rings
ID: noetherianity-of-formal-power-series-rings
For a commutative Noetherian ring, the ideals of lowest possible coefficients of an ideal in 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.
New to topics? Read the docs here!