Principal-unit group of a mixed-characteristic local field (source code)

= Principal-unit group of a mixed-characteristic local field
{title2=$1+\mathfrak m_K$}

If $K/\mathbb Q_p$ is finite of degree $d$, then as a topological <abelian group>
$$
1+\mathfrak m_K\cong\mu_{p^a}(K)\times\mathbb Z_p^d,
$$
where $\mu_{p^a}(K)$ is the finite group of all <roots of unity> in $K$ whose orders are <prime powers> dividing a power of $p$.