 Noetherianity of a formal power series ring

ID: noetherianity-of-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) ≅ R

. In the reverse direction, for an ideal

I

consider the ascending sequence of ideals of

R

formed by the coefficient of

x^{n}

I \cap x^{n} R [[x]]

. Stabilization and finite generation give a finite list of series that generate

I

by successive coefficient cancellation.

 New to topics? Read the docs here!