$\log_p x = \log_p(x^{p^k})/p^k$ on principal units

Proved

PadicLog.log_eq_log_pow_pow_div

by xuanji · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

leopoldtnumber-theoryp-adic

Let $K$ be a complete non-archimedean field of characteristic $0$ with $\|p\|<1$ , and let $\log_p$ be the $p$ -adic logarithm $\log_p x=\lim_n (x^{p^n}-1)/p^n$ . For every principal unit $x$ ( $\|x-1\|<1$ ) and every $k\ge 0$ ,

\log_p x=\frac{\log_p\left(x^{p^k}\right)}{p^k}.

Since $x^{p^k}\to1$ , for $k$ large $x^{p^k}$ lies in the ball where $\log_p$ is an isometry; this identity is the classical way (Washington §5.1) of extending $\log_p$ from a small neighbourhood of $1$ to all principal units.

Formalization Note Here $K$ is any complete, nontrivially normed, ultrametric field of characteristic zero with $\|p\|<1$ (e.g. a finite extension of $\mathbb{Q}_p$ , or a completion $K_{\mathfrak p}$ of a number field at $\mathfrak p\mid p$ ). PadicLog.log is the platform definition from Definitions.Def_PadicLog: $\log x=\lim_{n}(x^{p^n}-1)/p^n$ (a limUnder), previously only studied on the ball $\|x-1\|\le\|p\|^2$ ; PadicLog.logSeq x n $=(x^{p^n}-1)/p^n$ .

Preamble

import Definitions.Def_PadicLog

Formal statement

namespace PadicLog

theorem log_eq_log_pow_pow_div {p : ℕ} [Fact p.Prime] {K : Type*}
    [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K]
    [Fact (‖((p : ℕ) : K)‖ < 1)] [CharZero K] {x : K} (hx : ‖x - 1‖ < 1) (k : ℕ) :
    log (p := p) x = log (p := p) (x ^ p ^ k) / ((p : ℕ) : K) ^ k := by sorry

end PadicLog

Source

Washington, Introduction to Cyclotomic Fields (2nd ed., GTM 83), §5.1, Proposition 5.4 (the p-adic logarithm log_p on 1+pO extended to units; log_p(xy)=log_p x+log_p y; log_p x=0 iff x is a root of unity times a power of p) and Neukirch, Algebraic Number Theory, Ch. II, Prop. (5.4)–(5.5) (the logarithm on principal units U^(1), log x = lim (x^{p^n}-1)/p^n style extension). Iwasawa's limit form: Iwasawa, Lectures on p-adic L-functions, §2.

View graph

log⁡px=log⁡p(xpk)/pk\log_p x = \log_p(x^{p^k})/p^klogp​x=logp​(xpk)/pk on principal units

$\log_p x = \log_p(x^{p^k})/p^k$ on principal units