Kernel of the $p$ -adic logarithm on principal units is the torsion

Proved

PadicLog.log_eq_zero_iff

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 a principal unit $x\in K$ ( $\|x-1\|<1$ ),

\log_p x=0\iff x^n=1\text{ for some integer }n>0 .

That is, the kernel of $\log_p:U^{(1)}\to K$ is exactly the group of roots of unity contained in $U^{(1)}$ (necessarily of $p$ -power order). This is the principal-unit case of Washington, Prop. 5.4, and is the reason the $p$ -adic logarithm detects the $\mathbb{Z}_p$ -rank of a group of 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_zero_iff {p : ℕ} [Fact p.Prime] {K : Type*}
    [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K]
    [Fact (‖((p : ℕ) : K)‖ < 1)] [CharZero K] {x : K} (hx : ‖x - 1‖ < 1) :
    log (p := p) x = 0 ↔ ∃ n : ℕ, 0 < n ∧ x ^ n = 1 := 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

Kernel of the ppp-adic logarithm on principal units is the torsion

Kernel of the $p$ -adic logarithm on principal units is the torsion