Principal-unit logarithm (source code)

= 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,+).
$$