Brumer's theorem: $p$ -adic logarithms of algebraic numbers independent over $\mathbb{Q}$ are independent over $\overline{\mathbb{Q}}$

Proved

NumberField.Brumer.linearIndependent_log_algebraMap

by ebayuser · Oct 2, 2026 · Mathlib 0df444a (Lean v4.33.1)

iwasawa-theorynumber-theoryp-adictranscendenceunits

This is Brumer's theorem, the $p$ -adic analogue of Baker's theorem on linear forms in logarithms, in the form needed for Leopoldt's conjecture: $p$ -adic logarithms of algebraic numbers that are linearly independent over $\mathbb{Q}$ stay linearly independent over the algebraic numbers.

Let $p$ be a prime, $L$ a number field, and $w$ a prime of $\mathcal{O}_L$ above $p$ , with completion $L_w$ . Write $\log_p : L_w \to L_w$ for the $p$ -adic logarithm, which on the ball

B_w = \{\, x \in L_w : \|x - 1\| \le \|p\|^2 \,\}

is a homomorphism from multiplication to addition. Let $\alpha_1, \dots, \alpha_n \in L$ be elements whose images in $L_w$ lie in $B_w$ . If the logarithms $\log_p \alpha_1, \dots, \log_p \alpha_n$ are linearly independent over $\mathbb{Z}$ , then they are linearly independent over $L$ :

\sum_{i=1}^{n} c_i \log_p \alpha_i = 0,\ c_i \in L \quad\Longrightarrow\quad c_1 = \dots = c_n = 0 .

This is the transcendence input of the proof of Leopoldt's conjecture for abelian number fields. There, a vanishing character sum $\sum_\sigma \chi(\sigma) \log_p(\sigma\varepsilon)$ with algebraic coefficients $\chi(\sigma)$ is converted into an integral relation among the logarithms of the conjugates of a Minkowski unit, which is impossible. It is the only place in that proof where Diophantine approximation enters, and it is reusable in any argument that passes from a $p$ -adic relation with algebraic coefficients to a rational one.

Formalization Note Brumer's theorem is stated in $\mathbb{C}_p$ for algebraic $p$ -adic units with coefficients in the algebraic closure of $\mathbb{Q}$ inside $\mathbb{C}_p$ . The version here is a consequence of it: any finite set of algebraic numbers and coefficients lies in some number field $L$ , which is universally quantified, and the completion $L_w$ embeds continuously into $\mathbb{C}_p$ with the logarithm commuting with the embedding. Linear independence over $\mathbb{Q}$ is stated as linear independence over $\mathbb{Z}$ , which is equivalent because $L_w$ has characteristic zero. The elements are required to lie in the ball $B_w$ , where PadicLog.log of Definitions.Def_PadicLog is the genuine logarithm; Brumer's theorem for arbitrary algebraic units reduces to this case by raising to a power. $L$ acts on $L_w$ through the completion map, so LinearIndependent L is independence with coefficients in $L$ .

Preamble

import Definitions.Def_PadicLog

open NumberField

Formal statement

theorem NumberField.Brumer.linearIndependent_log_algebraMap (p : ℕ) [Fact p.Prime]
    (L : Type*) [Field L] [NumberField L] (w : Leopoldt.PrimesOver p L)
    (n : ℕ) (a : Fin n → L)
    (hball : ∀ i, ‖algebraMap L (w.1.adicCompletion L) (a i) - 1‖ ≤
      ‖((p : ℕ) : w.1.adicCompletion L)‖ ^ 2)
    (hli : LinearIndependent ℤ fun i =>
      PadicLog.log (p := p) (algebraMap L (w.1.adicCompletion L) (a i))) :
    LinearIndependent L fun i =>
      PadicLog.log (p := p) (algebraMap L (w.1.adicCompletion L) (a i)) := by sorry

Source

A. Brumer, On the units of algebraic number fields, Mathematika 14 (1967), 121-124, https://doi.org/10.1112/S0025579300003703, main theorem (p-adic analogue of Baker's theorem: p-adic logarithms of algebraic numbers linearly independent over Q are linearly independent over the algebraic closure of Q in C_p). Statement as in R. Sharifi, Iwasawa Theory (lecture notes), Theorem 1.5.17, https://www.math.ucla.edu/~sharifi/iwasawa.pdf, and L. C. Washington, Introduction to Cyclotomic Fields, 2nd ed., GTM 83, Section 5.5 (The p-adic regulator; Leopoldt's conjecture for abelian fields). Here specialized to elements of a number field L in the ball ‖x-1‖ ≤ ‖p‖^2 of the completion L_w, with Z-independence in place of Q-independence and L (universally quantified) in place of the algebraic closure of Q.

View graph

Brumer's theorem: ppp-adic logarithms of algebraic numbers independent over Q\mathbb{Q}Q are independent over Q‾\overline{\mathbb{Q}}Q​

Brumer's theorem: $p$ -adic logarithms of algebraic numbers independent over $\mathbb{Q}$ are independent over $\overline{\mathbb{Q}}$