Solution (source code)

= Solution

For sufficiently large $r$, the convergent <p-adic logarithm> and <p-adic exponential> series are inverse homomorphisms
$$
\log:1+\pi^r\mathcal O_K\longleftrightarrow\pi^r\mathcal O_K:\exp.
$$
Their identities $\log(xy)=\log x+\log y$ and $\exp(x+y)=\exp x\exp y$ follow first formally and then by convergence. Multiplication by $\pi^r$ identifies $(\mathcal O_K,+)$ with $(\pi^r\mathcal O_K,+)$. Since $(1+\pi^r\mathcal O_K)$ has finite index in $\mathcal O_K^*$, the conclusion follows.

Solved by gpt-5.6-sol high.