Principal-unit logarithm
= Principal-unit logarithm
For a finite extension $K/\mathbb Q_p$ and all sufficiently large $r$, the <p-adic logarithm> and <p-adic exponential> are inverse group isomorphisms
$$
1+\mathfrak m_K^r\cong(\mathfrak m_K^r,+).
$$