The $p$ -adic logarithm is a homomorphism on principal units

Proved

PadicLog.log_mul_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$ and let $\log_p$ be the $p$ -adic logarithm. For all principal units $x,y\in K$ (i.e. $\|x-1\|<1$ and $\|y-1\|<1$ ),

\log_p(xy)=\log_p x+\log_p y.

Hence $\log_p$ is a group homomorphism from the multiplicative group $U^{(1)}$ of principal units to the additive group of $K$ ; this is what makes the $p$ -adic regulator and the semilocal logarithm $\prod_{\mathfrak p\mid p}U^{(1)}_{\mathfrak p}\to\prod_{\mathfrak p\mid p}K_{\mathfrak p}$ homomorphisms.

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_mul_of_oneUnits {p : ℕ} [Fact p.Prime] {K : Type*}
    [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K]
    [Fact (‖((p : ℕ) : K)‖ < 1)] [CharZero K] {x y : K} (hx : ‖x - 1‖ < 1) (hy : ‖y - 1‖ < 1) :
    log (p := p) (x * y) = log (p := p) x + log (p := p) y := 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

The ppp-adic logarithm is a homomorphism on principal units

The $p$ -adic logarithm is a homomorphism on principal units