Logarithm isomorphism on deep principal units (source code)

= Logarithm isomorphism on deep principal units
{title2=$\log:1+\pi^r\mathcal O_K\cong\pi^r\mathcal O_K,\quad r>v_K(\ell)/(\ell-1)$}

For a mixed-characteristic <local field> with <residue characteristic> $\ell$, the <p-adic logarithm> and <p-adic exponential function> are mutually inverse continuous group homomorphisms on these domains. Bounds on the <valuations> of the denominators show that higher terms have greater <valuation> than the linear term. Dividing the logarithm by $\pi^r$ identifies the multiplicative <higher principal-unit group> with the additive integer ring; in particular it is torsion-free.