A global unit has zero semilocal logarithm precisely when it is torsion

Proved

Leopoldt.log_diagonalUnits_zero_iff_torsion

by xuanji · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

leopoldtnumber-theory

Let $\varepsilon$ be a global unit in a number field $K$ , and assume each of its components at primes above $p$ is close enough to $1$ for the local logarithm. The local logarithm of $\varepsilon$ vanishes at every place above $p$ if and only if $\varepsilon$ has finite multiplicative order. The semilocal torsion criterion and injectivity of the diagonal embedding of global units give the two directions.

Preamble

import Theorems.Thm_Leopoldt_semilocal_log_eq_zero_iff
import Theorems.Thm_Leopoldt_diagonalUnits_injective

open NumberField

Formal statement

namespace Leopoldt
theorem log_diagonalUnits_zero_iff_torsion (p : ℕ) [Fact p.Prime]
    (K : Type*) [Field K] [NumberField K]
    [∀ v : PrimesOver p K, CharZero (v.1.adicCompletion K)]
    (ε : (𝓞 K)ˣ)
    (hsmall : ∀ v : PrimesOver p K,
      ‖(((diagonalUnits p K ε v : (v.1.adicCompletionIntegers K)ˣ) :
          v.1.adicCompletionIntegers K) : v.1.adicCompletion K) - 1‖ < 1) :
    (∀ v : PrimesOver p K, PadicLog.log (p := p)
      (((diagonalUnits p K ε v : (v.1.adicCompletionIntegers K)ˣ) :
          v.1.adicCompletionIntegers K) : v.1.adicCompletion K) = 0) ↔
      ∃ n : ℕ, 0 < n ∧ ε ^ n = 1 := by sorry
end Leopoldt

Source

Formal consequence of Prove2Me theorems Leopoldt.semilocal_log_eq_zero_iff (82915127-01ab-499c-9b64-978bf6684c7a) and Leopoldt.diagonalUnits_injective (d1e6bbde-67ce-47ca-badc-651ce1c382eb).

View graph