Ring of formal power series over a field is a principal ideal domain
Solution 1:
The ring of a formal power series over a field is even more than a PID--it's a discrete valuation ring (hence a local ring). This follows from the lemma that a formal power series $f(X) = \sum_{n \geq 0} a_n X^n \in K[[X]]$ is a unit iff $a_0 \neq 0$. (More generally over a ring $R$, $f(X) \in R[[X]]^\times$ iff $a_0 \in R^\times$.) This shows that $(X)$ is the unique maximal ideal of $K[[X]]$. Thus the only ideals of $K[[X]]$ are $(X^n)$, so $f(X) = u(X) X^n$ for some $n \in \mathbb{Z}_{\geq 0}$ and $u(X) \in K[[X]]^\times$.