$\log_p(x^a)=a\log_p x$ for $a\in\mathbb{Z}_p$ on principal units

Proved

PadicLog.log_zpPow_of_oneUnits

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$ . For every principal unit $x\in K$ ( $\|x-1\|<1$ ) and every $p$ -adic integer $a\in\mathbb{Z}_p$ ,

\log_p\left(x^{a}\right)=a\,\log_p x,

where $x^a=\lim_n x^{a_n}$ for integers $a_n\to a$ is the $p$ -adic power of a principal unit and $a$ acts on $K$ through the canonical map $\mathbb{Z}_p\to K$ . So $\log_p:U^{(1)}\to K$ is $\mathbb{Z}_p$ -linear.

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$ . The $p$ -adic power is OneUnits.zpPow and $\mathbb{Z}_p\to K$ is PadicLog.zpCast.

Preamble

import Definitions.Def_PadicLog

Formal statement

namespace PadicLog

theorem log_zpPow_of_oneUnits {p : ℕ} [Fact p.Prime] {K : Type*}
    [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K]
    [Fact (‖((p : ℕ) : K)‖ < 1)] [CharZero K] {x : K} (hx : ‖x - 1‖ < 1) (a : ℤ_[p]) :
    log (p := p) (OneUnits.zpPow x a) = zpCast a * log (p := p) x := 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⁡p(xa)=alog⁡px\log_p(x^a)=a\log_p xlogp​(xa)=alogp​x for a∈Zpa\in\mathbb{Z}_pa∈Zp​ on principal units

$\log_p(x^a)=a\log_p x$ for $a\in\mathbb{Z}_p$ on principal units