TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 2026-10-02

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Dirichlet unit theorem

Statement

Assume the Axiom of Choice (The Axiom of Choice). For a number field $K$ of signature $(r_{1}, r_{2})$ there is an isomorphism $O_{K}^{\times} ≅ μ (K) \times Z^{r_{1} + r_{2} - 1}$ . In particular $O_{K}^{\times}$ is finitely generated of rank $r_{1} + r_{2} - 1$ and its torsion subgroup is $μ (K)$ .

Facts & Assumptions

Given: The Axiom of Choice, a number field $K$ of signature $(r_{1}, r_{2})$ with logarithmic embedding $λ$ (Logarithmic embedding of a number field), and the image $Λ : = λ (O_{K}^{\times})$ .

[F1]

For $x, y \in K^{\times}$ the multiplicativity of every embedding and of the complex modulus gives $∣ σ_{i} (x y) ∣ = ∣ σ_{i} x ∣ ∣ σ_{i} y ∣$ and $∣ τ_{j} (x y) ∣ = ∣ τ_{j} x ∣ ∣ τ_{j} y ∣$ , and $\log (x y) = \log x + \log y$ for positive reals; hence $λ (x y) = λ (x) + λ (y)$ , so $λ$ restricts to a group homomorphism $O_{K}^{\times} \to R^{r_{1} + r_{2}}$ (Logarithmic embedding of a number field, Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm, Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive).

[F2]

$\ker (λ ∣_{O_{K}^{\times}}) = μ (K)$ ; this kernel is finite and is exactly the torsion subgroup of $O_{K}^{\times}$ (Kernel of the unit logarithm is the roots of unity, The group $μ_{n} (K)$ of $n$ -th roots of unity in a field, and primitive $n$ -th roots of unity).

[F3]

$Λ$ is a full lattice in the hyperplane $H$ of the definition of $λ$ , of rank $r_{1} + r_{2} - 1$ ; hence $Λ = Z v_{1} \oplus \dots \oplus Z v_{r}$ for $R$ -linearly independent $v_{1}, \dots, v_{r} \in Λ$ and $r = r_{1} + r_{2} - 1$ (The logarithmic unit image is a full lattice).

[F4]

Every finitely generated abelian group $G$ has a decomposition $G ≅ Z^{s} \oplus T$ with $T$ its finite torsion subgroup, and the integer $s$ (the free rank) and the torsion subgroup are determined by $G$ (The fundamental theorem of finitely generated abelian groups from PID modules).

[F5]

The units of a commutative ring form an abelian group under multiplication; in particular $O_{K}^{\times}$ is an abelian group (The units of a ring are the invertible elements of its multiplicative monoid, and $R^{\times}$ is a group under multiplication; $0 \in R^{\times}$ only in the zero ring).

Proof

Proof technique: split the unit group by the logarithmic embedding. The image is a free abelian group whose rank is computed by the full-lattice theorem, and the kernel is the finite roots-of-unity group, so lifting a $Z$ -basis of the image exhibits $O_{K}^{\times}$ as $μ (K) \times Z^{r_{1} + r_{2} - 1}$ .

1.1F1F2

The restriction $λ ∣_{O_{K}^{\times}}$ is a group homomorphism onto $Λ$ with kernel $μ (K)$ , a finite group that coincides with the torsion subgroup of $O_{K}^{\times}$ .

1.2F3

By [F3] the image is $Λ = Z v_{1} \oplus \dots \oplus Z v_{r}$ with $v_{1}, \dots, v_{r} \in Λ$ $R$ -linearly independent and $r = r_{1} + r_{2} - 1$ ; choose once and for all units $u_{1}, \dots, u_{r} \in O_{K}^{\times}$ with $λ (u_{i}) = v_{i}$ , a selection of finitely many elements.

2.1F1step 1.1step 1.2

Let $u \in O_{K}^{\times}$ ; since $Λ$ is generated by $v_{1}, \dots, v_{r}$ there are unique integers $m_{1}, \dots, m_{r}$ with $λ (u) = \sum_{i} m_{i} v_{i} = λ (u_{1}^{m_{1}} \dots u_{r}^{m_{r}})$ , so $λ (u (u_{1}^{m_{1}} \dots u_{r}^{m_{r}})^{- 1}) = 0$ and hence $u (u_{1}^{m_{1}} \dots u_{r}^{m_{r}})^{- 1} = ζ$ for some $ζ \in μ (K)$ ; therefore $u = ζ u_{1}^{m_{1}} \dots u_{r}^{m_{r}}$ .

3.1F1step 1.2

The expression in step 2.1 is unique: if $ζ u_{1}^{m_{1}} \dots u_{r}^{m_{r}} = ζ^{'} u_{1}^{m_{1}^{'}} \dots u_{r}^{m_{r}^{'}}$ with $ζ, ζ^{'} \in μ (K)$ , then applying the homomorphism and using $λ (ζ) = λ (ζ^{'}) = 0$ gives $\sum_{i} (m_{i} - m_{i}^{'}) v_{i} = 0$ , hence $m_{i} = m_{i}^{'}$ for every $i$ by linear independence of the $v_{i}$ , and then $ζ = ζ^{'}$ .

4.1F5step 1.2step 2.1step 3.1

Consequently the map $μ (K) \times Z^{r} \to O_{K}^{\times}$ , $(ζ, m_{1}, \dots, m_{r}) \mapsto ζ u_{1}^{m_{1}} \dots u_{r}^{m_{r}}$ , is a bijective group homomorphism, because $O_{K}^{\times}$ is abelian and $u_{1}^{m_{1}} \dots u_{r}^{m_{r}} u_{1}^{n_{1}} \dots u_{r}^{n_{r}} = u_{1}^{m_{1} + n_{1}} \dots u_{r}^{m_{r} + n_{r}}$ ; hence $O_{K}^{\times} ≅ μ (K) \times Z^{r}$ with $r = r_{1} + r_{2} - 1$ , and $O_{K}^{\times}$ is finitely generated.

5.1F2F4step 4.1

Since $O_{K}^{\times}$ is finitely generated abelian, [F4] exhibits it as $Z^{s} \oplus T$ with $T$ its finite torsion subgroup; the displayed isomorphism of step 4.1 has free part $Z^{r_{1} + r_{2} - 1}$ and torsion factor $μ (K)$ , so by the uniqueness in [F4] the free rank is $s = r_{1} + r_{2} - 1$ and the torsion subgroup is $T = μ (K)$ .

6.1F3step 1.2∎

Choice accounting: the assumption AC enters only through the full-lattice theorem [F3]; the only selections made here are the finitely many units $u_{1}, \dots, u_{r}$ lifting a finite basis, and no choice over an infinite family occurs.

Depends on

Used by

Unit ranks by signature Corollary
System of fundamental units Definition
Two independent units in a real cubic field Example
S-unit theorem Theorem

Dependency tree · two levels

70 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

J. S. Milne, Algebraic Number Theory v3.08 (standard reference, not scraped)
William A. Stein, Algebraic Number Theory: A Computational Approach (standard reference, not scraped)
Andrew V. Sutherland, MIT 18.785 Lecture 15: Dirichlet's Unit Theorem (Fall 2021) (standard reference, not scraped)
Brian Conrad and Aaron Landesman, Math 154 Algebraic Number Theory (standard reference, not scraped)
Jurgen Neukirch, Algebraic Number Theory (Springer, 1999) (standard reference, not scraped)