TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-26

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 monic irreducible of degree $d$ over $F_{q}$ has the $d$ distinct roots $α, α^{q}, \dots, α^{q^{d - 1}}$

Statement

Let $F_{q}$ be a finite field of order $q$ , let $π \in F_{q} [t]$ be monic irreducible of degree $d \geq 1$ , and let $α$ be a root of $π$ in some extension field of $F_{q}$ . Then $F_{q} (α)$ is a finite field of order $q^{d}$ , the $d$ elements

$α, α^{q}, α^{q^{2}}, \dots, α^{q^{d - 1}}$

are pairwise distinct roots of $π$ lying in $F_{q} (α)$ ,

$π = \prod_{i = 0}^{d - 1} (t - α^{q^{i}}) in F_{q} (α) [t],$

and $F_{q} (α)$ is a splitting field of $π$ over $F_{q}$ (Polynomials that split and splitting fields of a polynomial or a family of polynomials), of degree $d$ over $F_{q}$ (The degree $[K : F] = \dim_{F} K$ of a finite field extension). In particular these $d$ elements are pairwise conjugate over $F_{q}$ (Conjugate algebraic elements over a field) and form a single orbit of the relative Frobenius. The list starts at $i = 0$ , so its first member is $α$ itself, and at $d = 1$ it is the single element $α \in F_{q}$ .

Facts & Assumptions

Given: A finite field $F_{q}$ of order $q \geq 2$ , a monic irreducible $π \in F_{q} [t]$ of degree $d \geq 1$ (Degree, leading coefficient and monic polynomial, with the zero polynomial having no degree), a root $α$ of $π$ in an extension field, and the field $K : = F_{q} (α)$ .

[L1]

If $K / F$ is a field extension and $a \in K$ is algebraic, there is a unique monic irreducible $m_{a} \in F [x]$ with $\ker ({ev}_{a}) = (m_{a})$ , and for every $f \in F [x]$ one has $f (a) = 0$ if and only if $m_{a} ∣ f$ (The evaluation kernel and the unique monic irreducible minimal polynomial of an algebraic element).

[L2]

If $a$ is algebraic over $F$ with minimal polynomial of degree $n$ , then $[F (a) : F] = n$ (An element is algebraic over $F$ if and only if its simple extension $F (a) / F$ is finite).

[L3]

If $[L : F_{q}] = m$ , then $L$ has an ordered $F_{q}$ -basis of length $m$ , and every element of $L$ has a unique coordinate list in that basis (The degree $[K : F] = \dim_{F} K$ of a finite field extension, Basis of a vector space: a linearly independent spanning subset; and ordered basis: an injective finite list whose image is a basis, A finite list $v : n \to V$ is an ordered basis if and only if every $x \in V$ equals $\sum_{i < n} λ_{i} v_{i}$ for exactly one $λ : n \to F$ ; those scalars are the coordinates of $x$ in that ordered basis).

[L4]

An extension $E / F_{q}$ of finite fields of degree $m$ is Galois with $Gal (E / F_{q}) = ⟨ σ_{q} ⟩$ cyclic of order $m$ , where $σ_{q} (x) = x^{q}$ (A finite extension of a finite field of order $q$ is Galois with cyclic Galois group generated by $x \mapsto x^{q}$ , The relative Frobenius $x \mapsto x^{q}$ of an extension of finite fields).

[L5]

Let $R$ be a commutative ring, $a \in R$ and $f \in R [x]$ . Then $f (a) = 0$ if and only if $x - a$ divides $f$ in $R [x]$ (Factor theorem over a commutative ring).

[L6]

A nonzero polynomial of degree $n$ over an integral domain has at most $n$ distinct roots in that domain (A nonzero polynomial of degree $n$ over an integral domain has at most $n$ distinct roots).

[L7]

If $F$ is a field with $q$ elements, then every $a \in F$ satisfies $a^{q} = a$ (A field with $q$ elements is the splitting field of $x^{q} - x$ over its prime subfield).

[L8]

Two elements algebraic over $F$ are conjugate over $F$ when they have the same minimal polynomial over $F$ (Conjugate algebraic elements over a field).

Proof

technique · direct

1.1

$π$ is the minimal polynomial of $α$ over $F_{q}$ : since $π (α) = 0$ , [L1] gives $m_{α} ∣ π$ , and $π$ is irreducible while $m_{α}$ is monic of degree at least one, so $π = m_{α}$ . Hence $[K : F_{q}] = d$ by [L2].

L1L2given

2.1

Fix the length- $d$ basis supplied by [L3]. Unique coordinates give a bijection $F_{q}^{d} \to K$ , so $∣ K ∣ = q^{d}$ and $K$ is a finite field. Now [L4] applies: $K / F_{q}$ is Galois with $Gal (K / F_{q}) = ⟨ σ_{q} ⟩$ cyclic of order $d$ , where $σ_{q} (x) = x^{q}$ .

step 1.1L3L4algebra

3.1

Each $σ_{q}^{i}$ fixes the coefficients of $π$ , which lie in $F_{q}$ , so applying the field homomorphism $σ_{q}^{i}$ to the equation $π (α) = 0$ gives $π (α^{q^{i}}) = 0$ : every $α^{q^{i}}$ is a root of $π$ lying in $K$ .

step 2.1L4given

4.1

The elements $α, α^{q}, \dots, α^{q^{d - 1}}$ are pairwise distinct. Suppose $α^{q^{i}} = α^{q^{j}}$ with $0 \leq i < j \leq d - 1$ and apply the automorphism $σ_{q}^{d - j}$ : since $x^{q^{d}} = x$ for every $x \in K$ by [L7] and step 2.1, this yields $α^{q^{r}} = α$ with $r : = i + d - j$ and $1 \leq r \leq d - 1$ . The set $S : = {x \in K : x^{q^{r}} = x}$ is the fixed set of the automorphism $σ_{q}^{r}$ , hence a subfield of $K$ ; it contains $F_{q}$ by [L7] and contains $α$ , so $K = F_{q} (α) \subseteq S$ . But $S$ is the root set in $K$ of the nonzero polynomial $t^{q^{r}} - t$ , so $∣ S ∣ \leq q^{r}$ by [L6], giving $q^{d} = ∣ K ∣ \leq q^{r} < q^{d}$ because $q \geq 2$ and $r < d$ . This is impossible.

step 2.1step 3.1L6L7algebra

5.1

The product $P : = \prod_{i = 0}^{d - 1} (t - α^{q^{i}})$ divides $π$ in $K [t]$ . Indeed, listing the distinct roots as $r_{0}, \dots, r_{d - 1}$ , [L5] writes $π = (t - r_{0}) g_{0}$ ; for $j \geq 1$ the equation $0 = π (r_{j}) = (r_{j} - r_{0}) g_{0} (r_{j})$ and $r_{j} \neq r_{0}$ in the field $K$ give $g_{0} (r_{j}) = 0$ , so the same step applies to $g_{0}$ with the remaining $d - 1$ distinct roots, and after $d$ such steps $π = P h$ for some $h \in K [t]$ .

step 3.1step 4.1L5

6.1

Both $π$ and $P$ are monic of degree $d$ , so $h$ is monic of degree $0$ , that is $h = 1$ and $π = P$ .

step 5.1givenalgebra

7.1

Consequently $π$ splits over $K$ , and $K = F_{q} (α)$ is generated over $F_{q}$ by the root $α$ ; since the subfield of $K$ generated over $F_{q}$ by all the roots of $π$ contains $α$ , it contains and hence equals $K$ , so $K$ is a splitting field of $π$ over $F_{q}$ . All $d$ roots share the minimal polynomial $π$ by step 1.1 and [L1], so they are pairwise conjugate over $F_{q}$ by [L8], and step 3.1 exhibits them as one orbit of $σ_{q}$ .

step 1.1step 3.1step 4.1step 6.1L1L8∎

Remarks

The index starts at zero. The orbit is $α^{q^{0}} = α, α^{q}, \dots, α^{q^{d - 1}}$ , so the factor $t - α$ is present in the product; dropping the term $i = 0$ would leave a polynomial of degree $d - 1$ that is not $π$ .
Where irreducibility is used. It enters twice: to identify $π$ with the minimal polynomial of $α$ in step 1.1, and through that identification to force $[K : F_{q}] = d$ , which is what makes the count in step 4.1 tight. For a reducible $π$ the conclusion fails outright, as $t^{2} - 1$ over $F_{3}$ shows: its roots $1$ and $- 1$ are not a Frobenius orbit.

Depends on

Used by

Dependency tree · two levels

54 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

K. Conrad, Finite Fields (expository blurb), Theorem 5.5 (standard reference, not scraped)
K. Conrad, Roots and Irreducibles (expository blurb), Theorem 5.4 (standard reference, not scraped)

A monic irreducible of degree dd over FqFq​ has the dd distinct roots α,αq,…,αqd−1α,αq,…,αqd−1