$r_1$ , $2r_2$ via roots of the minimal polynomial of a primitive element

Proved

DirichletUnitTheorem.nrPlaces_eq_card_roots_minpoly

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

algebraic-number-theorynumber-theory

Let $K$ be a number field and let $\alpha\in K$ be a primitive element, $K=\mathbb Q(\alpha)$ , with minimal polynomial $f\in\mathbb Q[x]$ . Then

$r_1$ is the number of real roots of $f$ , and
$2r_2$ is the number of non-real complex roots of $f$ .

This gives a practical way to compute the signature $(r_1,r_2)$ of $K$ .

Preamble

import Mathlib
open NumberField

Formal statement

namespace DirichletUnitTheorem

theorem nrPlaces_eq_card_roots_minpoly (K : Type*) [Field K] [NumberField K] (α : K)
    (hα : IntermediateField.adjoin ℚ {α} = ⊤) :
    InfinitePlace.nrRealPlaces K = ((minpoly ℚ α).rootSet ℝ).ncard ∧
      2 * InfinitePlace.nrComplexPlaces K =
        {z : ℂ | z ∈ (minpoly ℚ α).rootSet ℂ ∧ z.im ≠ 0}.ncard := by sorry

end DirichletUnitTheorem

Source

Wikipedia, "Dirichlet's unit theorem" (article supplied by the account owner as a PDF), lead section, first bullet of "Other ways of determining r1 and r2".

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. Let $K$ be a number field and $\alpha\in K$ such that the intermediate field $\mathbb Q(\alpha)$ generated by $\alpha$ over $\mathbb Q$ is all of $K$ . Let $f$ be the minimal polynomial of $\alpha$ over $\mathbb Q$ . Then both hold:

$r_1$ equals the number of distinct real numbers $x$ with $f(x)=0$ (cardinality of the root set of $f$ in $\mathbb R$ ; the count is taken with Set.ncard, which would be $0$ for an infinite set, but a nonzero polynomial has finitely many roots);
$2r_2$ equals the number of distinct complex numbers $z$ with $f(z)=0$ and $\operatorname{Im} z\neq 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).

View graph

r1r_1r1​, 2r22r_22r2​ via roots of the minimal polynomial of a primitive element

$r_1$ , $2r_2$ via roots of the minimal polynomial of a primitive element