TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 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.

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

Statement

Let $0 \neq f \in F [x]$ have degree $n$ . There is a splitting field $E / F$ , roots $α_{1}, \dots, α_{k}$ of $f$ in $E$ , and positive integers $d_{1}, \dots, d_{k}$ such that $E$ is spanned over $F$ by the root monomials $α_{1}^{e_{1}} \dots α_{k}^{e_{k}} (0 \leq e_{j} < d_{j}),$ and $d_{1} \dots d_{k} \leq n!$ . Thus $E$ has a spanning family of at most $n!$ explicit root monomials. When $n = 0$ , $k = 0$ , the sole empty monomial is $1$ , and $0! = 1$ .

Facts & Assumptions

Given: A field $F$ and a nonzero polynomial $f$ of degree $n$ .

[F1]

Strong induction permits proving a statement at degree $n$ from all smaller degrees (Strong (complete) induction).

[F2]

For $n \geq 1$ , one may adjoin a root $α$ and write $f = (x - α) g$ with $\deg g = n - 1$ (Kronecker's one-root step: adjoining a root removes a linear factor and lowers the remaining degree).

[F3]

The minimal polynomial of $α$ divides every polynomial vanishing at $α$ (The evaluation kernel and the unique monic irreducible minimal polynomial of an algebraic element).

[F4]

If that minimal polynomial has degree $d$ , then $F (α)$ has power basis $1, α, \dots, α^{d - 1}$ (A simple algebraic extension is its minimal-polynomial quotient and has power basis $1, a, \dots, a^{n - 1}$ and degree $n$ ).

[F5]

The factorial satisfies $0! = 1$ and $n! = n (n - 1)!$ for $n \geq 1$ (The factorial $n!$ and the falling factorial $n^{\underline{k}}$ , defined by recursion in $N$ ).

[F6]

A splitting field is generated by the roots over the base field (Polynomials that split and splitting fields of a polynomial or a family of polynomials).

[F7]

For nonzero polynomials over an integral domain, the degree of a product is the sum of the degrees (Over an integral domain, degrees add under multiplication of nonzero polynomials).

Proof

technique · strong induction on degree

1.1

Let $P (n)$ be the full assertion in the Statement, quantified over all base fields. For $n = 0$ , take $E = F$ and $k = 0$ . The vector $1$ spans $F$ and the number of displayed empty monomials is $1 = 0!$ .

F5F6base

1.2

Let $n \geq 1$ and assume $P (m)$ for every $m < n$ . By [F2], choose a root $α$ in the extension $K = F (α)$ and write $f = (x - α) g$ with $\deg g = n - 1$ . If the minimal polynomial of $α$ has degree $d$ , then $d \geq 1$ , [F3] and [F7] give $d \leq n$ , and [F4] gives the $F$ -basis $1, α, \dots, α^{d - 1}$ .

F2F3F4F7ih

2.1

Apply the induction hypothesis over $K$ to $g$ . It gives a splitting field $E / K$ spanned over $K$ by at most $(n - 1)!$ monomials in roots $α_{2}, \dots, α_{k}$ of $g$ . Multiplying those monomials by $1, α, \dots, α^{d - 1}$ spans $E$ over $F$ by monomials in roots of $f$ .

F4F6step 1.2ih

3.1

The number of resulting monomials is at most $d (n - 1)! \leq n (n - 1)! = n!$ by $d \leq n$ and [F5]. Moreover $E = K (roots of g) = F (α, roots of g)$ , so it is a splitting field of $f$ .

F5F6step 1.2step 2.1

4.1

The base case and inductive step establish $P (n)$ for every natural $n$ by [F1].

F1step 1.1step 1.2step 3.1discharge-induction∎

Depends on

Used by

The splitting field of x³-2 over ℚ is ℚ(³√2,ω) with ω=(-1+i√3)/2 Example

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 93 results over 18 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, Theorem 21.12 (standard reference, not scraped)
J. S. Milne, Fields and Galois Theory, Chapter 2 (standard reference, not scraped)

A degree-nn polynomial has a splitting field spanned over FF by at most n!n! explicit root monomials