ExampleConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-13

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.

The splitting field of $x^{3} - 2$ over $Q$ is $Q (\sqrt[3]{2}, ω)$ with $ω = (- 1 + i \sqrt{3}) / 2$

Example

Let $α = \sqrt[3]{2} > 0$ and $ω = (- 1 + i \sqrt{3}) / 2 \in C$ . The roots of $x^{3} - 2$ are $α, α ω, α ω^{2}$ , and its splitting field over $Q$ is $Q (α, ω)$ . It is spanned over $Q$ by at most $3! = 6$ root monomials.

Facts & Assumptions

Given: The polynomial $x^{3} - 2 \in Q [x]$ , the positive real root $α = \sqrt[3]{2}$ , and $ω = (- 1 + i \sqrt{3}) / 2$ .

[F1]

Positive real cube roots and square roots exist with the defining power equations (Existence and uniqueness of $n$ -th roots: a unique $a^{1 / n} \geq 0$ with $(a^{1 / n})^{n} = a$ , Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ ).

[F2]

The complex numbers form a field with $i^{2} = - 1$ and the usual coordinate arithmetic ( $C = R [x] / (x^{2} + 1)$ is a field, every element is uniquely $a + b i$ , and every nonzero element has inverse $(a - b i) / (a^{2} + b^{2})$ ).

[F3]

Once one nonzero root $α$ of $x^{n} - a$ is fixed, all roots are $ζ α$ for the $n$ th roots of unity $ζ$ (After adjoining one nonzero root $α$ of $x^{n} - a$ , all roots are $ζ α$ with $ζ^{n} = 1$ ).

[F4]

A degree- $n$ polynomial has a splitting field spanned by at most $n!$ root monomials (A degree- $n$ polynomial has a splitting field spanned over $F$ by at most $n!$ explicit root monomials).

[F5]

Eisenstein's criterion applies over $Q$ to the stated integer divisibility hypotheses (Eisenstein criterion over the integers).

[F6]

Any two splitting fields of a nonzero polynomial are isomorphic by an isomorphism fixing the base field (Any two splitting fields of a polynomial are isomorphic over the base field).

Verification

technique · direct calculation

1.1

By [F1], $α^{3} = 2$ and ${\sqrt{3}}^{2} = 3$ . Using [F2], direct calculation gives $ω^{2} + ω + 1 = 0$ , $ω \neq 1$ , and $x^{3} - 1 = (x - 1) (x - ω) (x - ω^{2})$ . Hence the cube roots of unity are exactly $1, ω, ω^{2}$ .

F1F2algebra

2.1

By [F3], the roots of $x^{3} - 2$ are exactly $α, α ω, α ω^{2}$ . They generate $Q (α, ω)$ because $α$ is a root and $ω = (α ω) / α$ , with $α \neq 0$ . Hence this field is the splitting field.

F3step 1.1

3.1

Eisenstein at $2$ makes $x^{3} - 2$ irreducible over $Q$ . Independently, [F4] gives a splitting field spanned by at most $3! = 6$ root monomials; an isomorphism from it to $Q (α, ω)$ supplied by [F6] fixes $Q$ and carries roots to roots by direct evaluation, so it transports that spanning family to one of the stated kind here.

F4F5F6step 2.1algebra∎

Depends on

Used by

Adjoining one root need not split the polynomial: ℚ(³√2) does not split x³-2 Counterexample

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 146 results over 22 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

T. Judson, Abstract Algebra: Theory and Applications, Example 21.15 (standard reference, not scraped)

The splitting field of x3−2x3−2 over QQ is Q(23,ω)Q(32​,ω) with ω=(−1+i3)/2ω=(−1+i3​)/2