The logarithmic image of the units is a lattice in the trace-zero hyperplane

Proved

DirichletUnitTheorem.logEmbedding_image_isLattice

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

algebraic-number-theorynumber-theory

Let $K$ be a number field and consider the map $\ell:\mathcal O_K^\times\to\mathbb R^{r+1}$ , indexed by the $r+1=r_1+r_2$ infinite places, given by

\ell(u) = \big(N_w\log\lvert u\rvert_w\big)_w.

Its image lies in the hyperplane $H=\{x : \sum_w x_w = 0\}$ and is a lattice there: it is a discrete subset of $\mathbb R^{r+1}$ and its $\mathbb R$ -linear span is exactly $H$ .

Formalization Note "Lattice in $H$ " is encoded as: the image is discrete in the subspace topology and its real span equals $H$ .

Preamble

import Mathlib
open NumberField

Formal statement

namespace DirichletUnitTheorem

theorem logEmbedding_image_isLattice (K : Type*) [Field K] [NumberField K] :
    DiscreteTopology (Set.range fun (u : (𝓞 K)ˣ) (w : InfinitePlace K) =>
        (w.mult : ℝ) * Real.log (w ((u : 𝓞 K) : K))) ∧
      (Submodule.span ℝ (Set.range fun (u : (𝓞 K)ˣ) (w : InfinitePlace K) =>
          (w.mult : ℝ) * Real.log (w ((u : 𝓞 K) : K))) : Set (InfinitePlace K → ℝ)) =
        {x | ∑ w, x w = 0} := by sorry

end DirichletUnitTheorem

Source

Wikipedia, "Dirichlet's unit theorem" (article supplied by the account owner as a PDF), section "The regulator", geometric interpretation ("has an image in the r-dimensional subspace ... consisting of all vectors whose entries have sum 0, and by Dirichlet's unit theorem the image is a lattice in this subspace").

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$ ). For an infinite place $w$ of $K$ , $\lvert x\rvert_w$ denotes the absolute value $\lvert\sigma(x)\rvert$ for an embedding $\sigma$ inducing $w$ , and $N_w$ is $1$ if $w$ is real and $2$ if $w$ is complex. $\log$ is the real logarithm (Mathlib's convention gives $\log 0 = 0$ , but units have $\lvert u\rvert_w>0$ ). Let $\ell(u)$ be the real vector indexed by the infinite places of $K$ with $w$ -coordinate $N_w\log\lvert u\rvert_w$ , for $u\in\mathcal O_K^\times$ , and let $\Lambda=\{\ell(u): u\in\mathcal O_K^\times\}\subseteq\mathbb R^{\text{places}}$ . Statement. For every number field $K$ , both hold:

$\Lambda$ , with the subspace topology from the product topology on $\mathbb R^{\text{places}}$ , is discrete;
the $\mathbb R$ -linear span of $\Lambda$ is exactly the set of vectors $x$ with $\sum_w x_w=0$ .

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).
Endorsed by mikedeng1 · Nov 8, 2026
Confirmed by the mission captain (proposal self-audit).

View graph