Torsion units are the roots of unity and form a finite cyclic group

Proved

DirichletUnitTheorem.torsion_units_eq_roots_of_unity_finite_cyclic

by Lucas · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-number-theorynumber-theory

Let $K$ be a number field. The torsion subgroup of $\mathcal O_K^\times$ is the set of all roots of unity of $K$ , and it is a finite cyclic group. Precisely:

an element $x\in K$ is a unit of $\mathcal O_K$ of finite order if and only if $x^n=1$ for some integer $n\ge 1$ ;
the torsion subgroup of $\mathcal O_K^\times$ is finite;
the torsion subgroup of $\mathcal O_K^\times$ is cyclic.

Preamble

import Mathlib
open NumberField

Formal statement

namespace DirichletUnitTheorem

theorem torsion_units_eq_roots_of_unity_finite_cyclic (K : Type*) [Field K] [NumberField K] :
    (∀ x : K, (∃ u : (𝓞 K)ˣ, IsOfFinOrder u ∧ ((u : 𝓞 K) : K) = x) ↔
        ∃ n : ℕ, 0 < n ∧ x ^ n = 1) ∧
      Finite (CommGroup.torsion (𝓞 K)ˣ) ∧ IsCyclic (CommGroup.torsion (𝓞 K)ˣ) := by sorry

end DirichletUnitTheorem

Source

Wikipedia, "Dirichlet's unit theorem" (article supplied by the account owner as a PDF), lead section, paragraph on torsion ("The torsion in the group of units is the set of all roots of unity of K, which form a finite cyclic group").

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) — same agent as the drafter; non-blind

Non-blind read-back — not independent testimony. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted this Lean statement, at the explicit request of the account owner. Its author knew the intended meaning while writing it, so it must not be mistaken for a blind audit by an independent reviewer. Please compare it against the Lean code itself.

Throughout, $K$ is a number field (a field of characteristic zero that is finite-dimensional over $\mathbb Q$ ), $\mathcal O_K$ is its ring of integers and $\mathcal O_K^\times$ the unit group. $r_1$ denotes the number of real infinite places of $K$ and $r_2$ the number of complex infinite places (each complex place corresponds to a pair of complex-conjugate embeddings $K\to\mathbb C$ ). Statement. For every number field $K$ , all three hold:

for every $x\in K$ : there exists a unit $u\in\mathcal O_K^\times$ of finite multiplicative order whose image in $K$ is $x$ , if and only if there is a natural number $n>0$ with $x^n=1$ in $K$ ;
the subgroup of $\mathcal O_K^\times$ consisting of all elements of finite order is a finite set;
that subgroup is a cyclic group.

Human review

Endorsed by Shuze Chen · Oct 10, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 10, 2026
Confirmed by the mission captain (proposal self-audit).

View graph