Ax's deduction: Brumer's theorem gives $r$ conjugates of a Minkowski unit with $\mathbb{Z}_p$-independent $p$-adic logarithms (totally real abelian fields)

This is the deduction of Leopoldt's conjecture for totally real abelian number fields from Brumer's theorem: Ax's plan, carried out by Brumer in 1967 once the $p$-adic Baker theorem was available.

Let $p$ be a prime and $K$ a totally real number field that is Galois over $\mathbb{Q}$ with abelian Galois group $G$, so that the unit rank is $r = [K:\mathbb{Q}] - 1$. Let $\varepsilon \in \mathcal{O}_K^\times$ be a Minkowski unit, that is, a unit whose Galois conjugates $\sigma\varepsilon$ ($\sigma \in G$) generate a subgroup of finite index in $\mathcal{O}_K^\times$, and assume that every conjugate lies in the ball $\|x - 1\| \le \|p\|^2$ at every prime $v$ of $K$ above $p$. For a unit $u$ write

for its semilocal $p$-adic logarithm vector. Assume Brumer's theorem: for every number field $L$, every prime $w$ of $L$ above $p$ and every finite family of elements of $L$ lying in the ball at $w$, $\mathbb{Z}$-linear independence of their $p$-adic logarithms implies $L$-linear independence. Then there are $r$ Galois conjugates $\sigma_1\varepsilon, \dots, \sigma_r\varepsilon$ whose vectors

are linearly independent over $\mathbb{Z}_p$.

By the criterion Leopoldt.leopoldtConjecture_iff_exists_linearIndependent_log_conj, the conclusion is Leopoldt's conjecture for $K$. The classical argument fixes a prime $v_0 \mid p$ and considers the group determinant $\det\bigl(\log_p \tau\sigma^{-1}\varepsilon\bigr)_{\sigma,\tau \in G}$, which factors as $\prod_{\chi} \sum_{\sigma} \chi(\sigma)\log_p(\sigma\varepsilon)$ over the characters $\chi$ of $G$. The trivial character contributes $\log_p N_{K/\mathbb{Q}}(\varepsilon) = 0$. For a nontrivial $\chi$ the character sum is a linear form in the logarithms of the conjugates with coefficients in a cyclotomic extension of $K$; if it vanished, Brumer's theorem would give an integral relation among the conjugates of $\varepsilon$, that is, a product of conjugates equal to a root of unity, which contradicts the finite index. Hence the matrix of logarithms has rank $r$, and Galois covariance of the semilocal logarithm transfers the independence from the single place $v_0$ to the semilocal vectors.

Formalization Note Brumer's theorem is taken as the hypothesis hB, stated exactly as the platform theorem NumberField.Brumer.linearIndependent_log_algebraMap and quantified over all number fields $L$ in the same universe as $K$, so that a proof may apply it to $L = K(\zeta_d)$ and its primes above $p$. The hypotheses on $\varepsilon$ are those of the criterion theorem: finite index of the subgroup generated by the conjugates, and the ball condition at every prime above $p$. The conjugate $\sigma\varepsilon$ is Units.map (RingOfIntegers.mapRingEquiv σ.toRingEquiv).toMonoidHom ε, and Fin (Units.rank K) → (K ≃ₐ[ℚ] K) selects the $r$ conjugates. Mathlib has no group-determinant formula; a proof must either supply it or argue directly with characters of the finite abelian group $G$ over the cyclotomic field. The Galois covariance of the semilocal logarithm is available as Leopoldt.log_diagonalUnits_conj.