Finite coefficient field in positive-characteristic local fields (${\mathbb{F}}_q\hookrightarrow {\mathcal{O}}_K,a^q=a$)

For a characteristic-p local field with residue field ${\mathbb{F}}_q$, the simple roots of $X^q-X$ lift uniquely by Hensel lemma. Their lifts form a copy of ${\mathbb{F}}_q$, since qth powers preserve addition and multiplication. Choose a uniformizer $\pi$. Repeatedly subtracting the lifted residue and dividing by $\pi$ produces a unique convergent expansion ${\sum }_{i\ge 0}{a}_i{\pi }^i$ for each integral element. Allowing finitely many negative powers gives a valued-field isomorphism $K\cong {\mathbb{F}}_q((T))$, $T\mapsto \pi$.