Fundamental units of the cyclic cubic field $\mathbb Q(\alpha)$ , $\alpha^3+\alpha^2-2\alpha-1=0$

Proved

DirichletUnitTheorem.cyclic_cubic_fundamental_units

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

algebraic-number-theorynumber-theory

Let $K$ be a number field with $[K:\mathbb Q]=3$ containing an element $\alpha$ with $\alpha^3+\alpha^2-2\alpha-1=0$ (so $K=\mathbb Q(\alpha)$ is the cyclic cubic field of discriminant $49$ ). Put $\varepsilon_1=\alpha^2+\alpha-1$ and $\varepsilon_2=2-\alpha^2$ . Then $\{\varepsilon_1,\varepsilon_2\}$ is a basis of the unit group of $K$ modulo roots of unity:

$\varepsilon_1,\varepsilon_2\neq0$ ;
every unit $u$ of $\mathcal O_K$ can be written as $u=\zeta\,\varepsilon_1^{a}\varepsilon_2^{b}$ with $\zeta$ a root of unity and $a,b\in\mathbb Z$ ;
if $\varepsilon_1^{a}\varepsilon_2^{b}$ is a root of unity, then $a=b=0$ .

Formalization Note Powers with negative integer exponents are taken in the field $K$ .

Preamble

import Mathlib
open NumberField

Formal statement

namespace DirichletUnitTheorem

theorem cyclic_cubic_fundamental_units (K : Type*) [Field K] [NumberField K]
    (hK : Module.finrank ℚ K = 3) (α : K) (hα : α ^ 3 + α ^ 2 - 2 * α - 1 = 0) :
    (α ^ 2 + α - 1) ≠ 0 ∧ (2 - α ^ 2) ≠ 0 ∧
    (∀ u : (𝓞 K)ˣ, ∃ ζ : (𝓞 K)ˣ, IsOfFinOrder ζ ∧ ∃ a b : ℤ,
        ((u : 𝓞 K) : K) = ((ζ : 𝓞 K) : K) * (α ^ 2 + α - 1) ^ a * (2 - α ^ 2) ^ b) ∧
    (∀ a b : ℤ, (∃ n : ℕ, 0 < n ∧ ((α ^ 2 + α - 1) ^ a * (2 - α ^ 2) ^ b) ^ n = 1) →
        a = 0 ∧ b = 0) := by sorry

end DirichletUnitTheorem

Source

Wikipedia, "Dirichlet's unit theorem" (article supplied by the account owner as a PDF), section "The regulator", Examples, third bullet (cyclic cubic field; Cohen 1993, Table B.4).

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.

Let $K$ be a number field with $[K:\mathbb Q]=3$ and $\alpha\in K$ with $\alpha^3+\alpha^2-2\alpha-1=0$ ; write $\varepsilon_1=\alpha^2+\alpha-1$ , $\varepsilon_2=2-\alpha^2$ (elements of $K$ ). Statement. All of the following hold:

$\varepsilon_1\neq0$ and $\varepsilon_2\neq0$ ;
for every unit $u\in\mathcal O_K^\times$ there are a unit $\zeta\in\mathcal O_K^\times$ of finite order and integers $a,b$ such that, in $K$ , $u=\zeta\,\varepsilon_1^{a}\varepsilon_2^{b}$ (integer powers in the field $K$ ; Mathlib's convention $0^{-1}=0$ is irrelevant given item 1);
for all integers $a,b$ : if $(\varepsilon_1^{a}\varepsilon_2^{b})^n=1$ for some natural number $n>0$ , then $a=0$ and $b=0$ .

Note that item 2 does not itself assert that $\varepsilon_1,\varepsilon_2$ lie in $\mathcal O_K^\times$ .

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

Fundamental units of the cyclic cubic field Q(α)\mathbb Q(\alpha)Q(α), α3+α2−2α−1=0\alpha^3+\alpha^2-2\alpha-1=0α3+α2−2α−1=0

Fundamental units of the cyclic cubic field $\mathbb Q(\alpha)$ , $\alpha^3+\alpha^2-2\alpha-1=0$