The torsion subgroup of the semilocal units $U$ is finite

Proved

Leopoldt.finite_torsion_semilocalUnits

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

leopoldtnumber-theoryp-adic

Let $K$ be a number field, $p$ a prime, and

U=\prod_{\mathfrak p\mid p}\mathcal O_{\mathfrak p}^\times

the group of semilocal units at $p$ (the platform's SemilocalUnits p K). Then the torsion subgroup

U_{\mathrm{tors}}=\{u\in U:\ u^n=1\text{ for some }n\ge 1\}=\prod_{\mathfrak p\mid p}\mu(K_{\mathfrak p})

is finite; equivalently each completion $K_{\mathfrak p}$ contains only finitely many roots of unity.

This finiteness is what makes $\mathbb{Z}_p$ -ranks of subgroups of $U$ well behaved: up to a finite group, $U$ is its principal part, a finitely generated $\mathbb{Z}_p$ -module.

Preamble

import Definitions.Def_LeopoldtDefect

Formal statement

namespace Leopoldt

theorem finite_torsion_semilocalUnits (p : ℕ) [Fact p.Prime] (K : Type*) [Field K]
    [NumberField K] : Finite (CommGroup.torsion (SemilocalUnits p K)) := by sorry

end Leopoldt

Source

J. Neukirch, Algebraic Number Theory, Ch. II §5, Prop. 5.7 (

\mathcal O^\times\cong\mu_{q-1}\times U^{(1)}

U^{(1)}\cong\mu_{p^a}\times\mathbb Z_p^d

; in particular

\mu(K_\mathfrak p)

is finite); P. Mihăilescu, arXiv:1105.4544, §1.1

View graph

The torsion subgroup of the semilocal units UUU is finite

The torsion subgroup of the semilocal units $U$ is finite