ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)audited 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.

Units of $Q$ and the imaginary quadratic fields

Example

Assume the Axiom of Choice. For $K = Q$ one has $O_{K} = Z$ and $O_{K}^{\times} = {\pm 1}$ . For $K = Q (i)$ one has $O_{K} = Z [i]$ and $O_{K}^{\times} = {\pm 1, \pm i} = μ_{4} (K)$ . For $K = Q (\sqrt{- 3})$ , with $ω = (1 + \sqrt{- 3}) / 2$ , one has $O_{K} = Z [(1 + \sqrt{- 3}) / 2] = Z [ω]$ and $O_{K}^{\times} = μ_{6} (K) = {\pm 1, \pm ω, \pm ω^{2}}$ . All three unit groups are finite of rank $0$ .

Facts & Assumptions

Given: The Axiom of Choice and the three number fields $Q$ , $Q (i) = Q (\sqrt{- 1})$ and $Q (\sqrt{- 3})$ , with the element $ω : = (1 + \sqrt{- 3}) / 2$ (number field).

[F1]

The ring of integers $O_{Q}$ is the integral closure of $Z$ in $Q$ (Ring of integers); a rational number integral over $Z$ is an integer (The rational algebraic integers are exactly the integers), and conversely every integer $n$ is a root of the monic polynomial $X - n$ . Hence $O_{Q} = Z$ .

[F2]

For squarefree $d \neq 1$ one has $O_{Q (\sqrt{d})} = Z [(1 + \sqrt{d}) / 2]$ if $d \equiv 1 (m o d 4)$ and $O_{Q (\sqrt{d})} = Z [\sqrt{d}]$ otherwise (Integers in a quadratic field). Since $- 1 \equiv 3 (m o d 4)$ and $- 3 \equiv 1 (m o d 4)$ , this gives $O_{Q (i)} = Z [\sqrt{- 1}] = Z [i]$ and $O_{Q (\sqrt{- 3})} = Z [(1 + \sqrt{- 3}) / 2] = Z [ω]$ .

[F3]

For a number field $K$ and $u \in O_{K}$ , the element $u$ is a unit of $O_{K}$ if and only if $N_{K / Q} (u) = \pm 1$ (A number-field unit is exactly an algebraic integer of norm plus or minus one).

[F4]

Let $d \in Q$ be nonsquare and put $K = Q (\sqrt{d})$ . A degree- $2$ polynomial over $Q$ is irreducible exactly when it has no rational root (A polynomial of degree two or three over a field is irreducible exactly when it has no root in the field), and $d$ is not a square in $Q$ , so $X^{2} - d$ is the minimal polynomial of $\sqrt{d}$ over $Q$ (The evaluation kernel and the unique monic irreducible minimal polynomial of an algebraic element) and $[K : Q] = 2$ . By the correspondence between $F$ -embeddings and distinct roots of the minimal polynomial ( $F$ -embeddings of $F (α)$ into an algebraically closed field correspond to the distinct roots of $m_{α}$ ), the two $Q$ -embeddings of $K$ into $C$ send $\sqrt{d}$ to $\sqrt{d}$ and to $- \sqrt{d}$ ; since $char Q = 0$ , norm and trace are the product and sum over these embeddings (Norm and trace from embeddings, with the inseparable exponent in the norm formula). Hence for $α = a + b \sqrt{d}$ with $a, b \in Q$ , $N_{K / Q} (α) = (a + b \sqrt{d}) (a - b \sqrt{d}) = a^{2} - d b^{2} .$

[F5]

The units of $Z$ are exactly $1$ and $- 1$ ( $(Z, \cdot, 1)$ is a commutative monoid whose group of units is ${1, - 1}$ ; equivalently $u ∣ 1$ holds exactly for $u = 1$ and $u = - 1$ ).

[F6]

For $n \geq 1$ , $μ_{n} (K) = {x \in K : x^{n} = 1}$ is the set of $n$ -th roots of unity in $K$ , and $μ (K)$ denotes the group of all roots of unity in $K$ , the union of the subgroups $μ_{n} (K)$ (The group $μ_{n} (K)$ of $n$ -th roots of unity in a field, and primitive $n$ -th roots of unity).

[F7]

If $x \in K$ satisfies $x^{n} = 1$ for some $n \geq 1$ , then $x$ is a root of the monic polynomial $T^{n} - 1 \in Z [T]$ , hence is integral over $Z$ (Integral elements over a commutative ring and algebraic integers) and lies in $O_{K}$ , the integral closure of $Z$ in $K$ (Ring of integers); also $x^{- 1} = x^{n - 1} \in O_{K}$ , so $x \in O_{K}^{\times}$ . In particular every root of unity in $K$ is a unit of $O_{K}$ , that is $μ (K) \subseteq O_{K}^{\times}$ .

[F8]

The unit rank $r_{1} + r_{2} - 1$ is $0$ exactly for $Q$ and for imaginary quadratic fields, and in the rank-zero cases $O_{K}^{\times} = μ (K)$ is finite (Unit ranks by signature); a quadratic field $Q (\sqrt{d})$ with $d < 0$ has no real embedding and two complex conjugate embeddings, hence signature $(0, 1)$ (Archimedean embeddings and signature).

[A1]

The Axiom of Choice is assumed; it is used only through the rank-zero unit structure [F8] (The Axiom of Choice).

Verification

technique · compute the unit group of each of the three rings of integers by solving the norm equation $N(u)=\pm1$ with the elementary norm formula for quadratic fields, and identify the results with the groups of fourth and sixth roots of unity

1.1F1F5F6F7

$O_{Q} = Z$ and $O_{Q}^{\times} = Z^{\times} = {\pm 1}$ : the rational units are the units of $Z$ , and $\pm 1$ are roots of unity while every element of $μ (Q)$ is a unit of $Z$ by [F7], so $μ (Q) = {\pm 1}$ as well.

1.2F2

By [F2] and the congruences $- 1 \equiv 3 (m o d 4)$ , $- 3 \equiv 1 (m o d 4)$ one has $O_{Q (i)} = Z [i] = {a + b i : a, b \in Z}$ and $O_{Q (\sqrt{- 3})} = Z [ω] = {a + b ω : a, b \in Z}$ , where $ω = (1 + \sqrt{- 3}) / 2$ .

1.3F4

Applying [F4] with the nonsquare rational $d = - 1$ to $a + b i = a + b \sqrt{- 1}$ with $a, b \in Z \subseteq Q$ gives $N_{Q (i) / Q} (a + b i) = a^{2} + b^{2}$ .

1.4F4algebra

Writing $a + b ω = (a + b / 2) + (b / 2) \sqrt{- 3}$ with $a, b \in Z$ and applying [F4] with the nonsquare rational $d = - 3$ gives $N_{Q (\sqrt{- 3}) / Q} (a + b ω) = (a + b / 2)^{2} + 3 (b / 2)^{2} = a^{2} + a b + b^{2}$ .

2.1F3step 1.3algebra

By [F3] and step 1.3, $a + b i \in Z [i]$ is a unit if and only if $a^{2} + b^{2} = \pm 1$ . Since $a^{2} + b^{2} \geq 0$ , this is the equation $a^{2} + b^{2} = 1$ with $a, b \in Z$ ; then $a^{2} \leq 1$ , $∣ a ∣ \leq 1$ , and $b^{2} = 1 - a^{2}$ , so either $a = 0$ and $b = \pm 1$ or $b = 0$ and $a = \pm 1$ . Hence $O_{Q (i)}^{\times} = {1, - 1, i, - i}$ .

2.2F3step 1.4algebra

By [F3] and step 1.4, $a + b ω \in Z [ω]$ is a unit if and only if $a^{2} + a b + b^{2} = \pm 1$ . Since $4 (a^{2} + a b + b^{2}) = (2 a + b)^{2} + 3 b^{2} \geq 0$ , the value $- 1$ cannot occur, and $a^{2} + a b + b^{2} = 1$ is equivalent to $(2 a + b)^{2} + 3 b^{2} = 4$ ; then $3 b^{2} \leq 4$ with $b \in Z$ forces $b \in {- 1, 0, 1}$ . If $b = 0$ then $(2 a)^{2} = 4$ gives $a = \pm 1$ ; if $b = 1$ then $(2 a + 1)^{2} = 1$ gives $a = 0$ or $a = - 1$ ; if $b = - 1$ then $(2 a - 1)^{2} = 1$ gives $a = 1$ or $a = 0$ .

3.1step 2.2algebra

Direct computation in $Z [ω]$ gives $ω^{2} = \frac{- 1 + \sqrt{- 3}}{2} = ω - 1$ and $ω^{3} = ω \cdot ω^{2} = ω^{2} - ω = (ω - 1) - ω = - 1$ , hence $ω^{6} = 1$ . Since $1, ω, ω - 1, - 1$ have pairwise different coordinates in the $Z$ -basis $(1, ω)$ of $Z [ω]$ , the elements $ω, ω^{2}, ω - 1$ are all different from $1$ , and the six units found in step 2.2 are exactly $ω^{0}, ω^{1}, ω^{2}, ω^{3} = - 1, ω^{4} = - ω, ω^{5} = - (ω - 1)$ .

3.2F6F7step 2.1

Each of the four elements $1, - 1, i, - i$ of $O_{Q (i)}^{\times}$ satisfies $x^{4} = 1$ , so $O_{Q (i)}^{\times} \subseteq μ_{4} (Q (i))$ by [F6], while $μ_{4} (Q (i)) \subseteq O_{Q (i)}^{\times}$ by [F7]; hence $O_{Q (i)}^{\times} = μ_{4} (Q (i)) = {\pm 1, \pm i}$ .

4.1F6F7step 2.2step 3.1

Each of the six units found in step 2.2 is a power of $ω$ by step 3.1, hence satisfies $x^{6} = 1$ ; therefore $O_{Q (\sqrt{- 3})}^{\times} \subseteq μ_{6} (Q (\sqrt{- 3}))$ by [F6], and $μ_{6} (Q (\sqrt{- 3})) \subseteq O_{Q (\sqrt{- 3})}^{\times}$ by [F7]; hence $O_{Q (\sqrt{- 3})}^{\times} = μ_{6} (Q (\sqrt{- 3})) = {\pm 1, \pm ω, \pm ω^{2}}$ , because $ω^{3} = - 1$ gives ${ω^{0}, \dots, ω^{5}} = {\pm 1, \pm ω, \pm ω^{2}}$ .

5.1F8step 1.1step 3.2step 4.1

Finally $Q$ has signature $(1, 0)$ and both imaginary quadratic fields have signature $(0, 1)$ , so [F8] gives unit rank $r_{1} + r_{2} - 1 = 0$ for all three fields and exhibits the unit groups as finite torsion groups $μ (K)$ ; the computed groups ${\pm 1}$ , ${\pm 1, \pm i}$ and ${\pm 1, \pm ω, \pm ω^{2}}$ have $2$ , $4$ and $6$ elements.

6.1A1F8∎

Choice accounting: AC is used only through the rank-zero structure [F8]; the norm computations, the enumeration of the norm-one solutions, and the powers of $ω$ are elementary computations in $Z$ and $Z [ω]$ and use no choice.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

80 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)
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)

Units of QQ and the imaginary quadratic fields