formal power series over field
Theorem. If is a field, then the ring of formal power series is a discrete valuation ring with
its unique maximal ideal.
Proof. We show first that an arbitrary ideal of is a principal ideal. If , the thing is ready. Therefore, let . Take an element
of such that it has the least possible amount of successive zero coefficients in its beginning; let its first non-zero coefficient be . Then
Here we have in the parentheses an invertible formal power series , whence get the equation
implying and consequently .
For obtaining the reverse inclusion, suppose that
is an arbitrary nonzero element of where . Because , we may write
This equation says that , whence .
Thus we have seen that is the principal ideal , so that is a principal ideal domain.
Now, all ideals of the ring form apparently the strictly descending chain
whence the ring has the unique maximal ideal . A principal ideal domain with only one maximal ideal is a discrete valuation ring.