Let $K$ be a finite extension of the field of $p$-adic numbers $\mathbb{Q}_p$, call $\mathcal{O}_K$ the valuation ring of $K$ (i.e. the set of elements of $K$ with valuation greater or equal than zero). Call $\mathcal{O}_K^\times$ the multiplicative group of units of $\mathcal{O}_K$ (i.e. the group of elements of $K$ with zero valuation).
I have read that there is a group isomorphism \begin{equation*} \mathcal{O}_K^\times\cong \mathbb{Z}_p^{a}\times U \end{equation*} for some $a\in\mathbb{N}$ and $U$ finite group. Could you tell me why, or where I can find a proof of this result?
I know that $\mathcal{O}_K\cong \mathbb{Z}_p^{[K:\mathbb{Q}_p]}$ as $\mathbb{Z}_p$-modules, but this isomorphism only involves the additive structure of $\mathcal{O}_K$.
This should be in any algebraic number theory textbook that mentions the $p$-adics e.g. Neukirch. Here is a rough sketch; the technical details on the $p$-adic logarithm are in Neukirch and other places.
Let $\pi$ be a uniformizer. One knows that the higher unit groups, $U^{(n)} = 1 + (\pi)^n$, are of finite index in $\mathcal O_K^\times$ and that the logarithm gives a homomorphism from $U^{(n)}$ under multiplication to $(\pi)^n$ under addition as $\mathbb Z_p$-modules. For sufficiently large $n$, this is an isomorphism. Since $(\pi)^n$ is isomorphic to $\mathcal O_K$ (under addition), we can see that it is a free $\mathbb Z_p$-module of rank equal to the degree of $K$ over $\mathbb Q_p$. Therefore, $\mathcal O_K^\times$ is a $\mathbb Z_p$-module of rank $[K:\mathbb Q_p]$ (using the finite index fact). So we can decompose it into a free part of that rank times some torsion; the torsion of $\mathcal O_K^\times$ is clearly given by the roots of unity.
Putting it all together, we obtain a slightly more precise version of your claim: $$\mathcal O_K^\times \cong \mathbb Z_p^{[K:\mathbb Q_p]} \times \{\textrm{roots of unity in $K$}\}$$