formal power series over field

Theorem.  If $K$ is a field, then the ring $K[[X]]$ of formal power series is a discrete valuation ring with$(X)$ its unique maximal ideal.

Proof.  We show first that an arbitrary ideal $I$ of $K[[X]]$ is a principal ideal.  If $I=(0)$,  the thing is ready.  Therefore, let  $I\ne (0)$.  Take an element

$$f(X):=\sum _{i=0}^{\mathrm{\infty }}{a}_i{X}^i$$

of $I$ such that it has the least possible amount of successive zero coefficients in its beginning; let its first non-zero coefficient be $a_k$.  Then

$$f(X)=X^k(a_k+a_{k+1}X+\mathrm{\dots }).$$

Here we have in the parentheses an invertible formal power series $g(X)$, whence get the equation

$$X^k=f(X){[g(X)]}^{-1}$$

implying  $X^k\in I$  and consequently  $(X^k)\subseteq I$.
For obtaining the reverse inclusion, suppose that

$$h(X):=b_n{X}^n+b_{n+1}{X}^{n+1}+\mathrm{\dots }$$

is an arbitrary nonzero element of $I$ where  $b_n\ne 0$.  Because  $n\ge k$,  we may write

$$h(X)=X^k(b_n{X}^{n-k}+b_{n+1}{X}^{n-k+1}+\mathrm{\dots }).$$

This equation says that  $h(X)\in (X^k)$,  whence  $I\subseteq (X^k)$.
Thus we have seen that $I$ is the principal ideal $(X^k)$, so that $K[[X]]$ is a principal ideal domain.
Now, all ideals of the ring $K[[X]]$ form apparently the strictly descending chain

$$(X)\supset (X^2)\supset (X^3)\supset \mathrm{\dots }\supset (0),$$

whence the ring has the unique maximal ideal $(X)$.  A principal ideal domain with only one maximal ideal is a discrete valuation ring.