TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 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.

Every finite cyclic extension has a normal basis

Statement

Let $K / F$ be a finite Galois extension whose Galois group is cyclic, say $Gal (K / F) = ⟨ σ ⟩$ of order $n = [K : F]$ . Then $K / F$ has a normal basis (Normal bases of a finite Galois extension): there is $α \in K$ for which

$(α, σ α, \dots, σ^{n - 1} α)$

is an ordered $F$ -basis of $K$ (Basis of a vector space: a linearly independent spanning subset; and ordered basis: an injective finite list whose image is a basis).

Facts & Assumptions

Given: A finite Galois extension $K / F$ with $Gal (K / F) = ⟨ σ ⟩$ cyclic of order $n$ ; by [L6] $\dim_{F} K = [K : F] = n$ , and $σ$ is an $F$ -linear endomorphism of the $F$ -vector space $K$ , written $T$ when regarded as such. Evaluation of a polynomial at $T$ is that of Polynomial evaluation at an endomorphism: $p (T) = \sum_{k} a_{k} T^{k}$ .

[L1]

Let $G$ be a group and $K$ a field. Every finite family of distinct group homomorphisms $G \to K^{\times}$ is linearly independent over $K$ as a family of functions (Dedekind's linear independence theorem for distinct characters).

[L2]

For every endomorphism $T$ of a finite-dimensional $F$ -vector space, $Ann (T) = {p \in F [x] : p (T) = 0}$ is a nonzero ideal with a unique monic generator $μ_{T}$ , and $p (T) = 0$ if and only if $μ_{T} ∣ p$ (The annihilator ideal is nonzero and has a unique monic generator; $p (T) = 0$ if and only if $μ_{T} ∣ p$ , The annihilator set $Ann (T) = {p \in F [x] : p (T) = 0}$ ; once existence is proved, its unique monic generator $μ_{T}$ is the minimal polynomial).

[L3]

For $A \in M_{n} (F)$ the polynomial $χ_{A}$ is monic of degree $n$ ( $χ_{A} (x)$ is monic of degree $n$ ; for $n \geq 1$ its $x^{n - 1}$ coefficient is $- tr (A)$ and its constant coefficient is $(- 1)^{n} \det (A)$ , while $χ_{0 \times 0} = 1$ ); $χ_{T}$ is defined as $χ_{[T]_{B}}$ for any ordered basis $B$ and is independent of it (The basis-independent characteristic polynomial $χ_{T}$ of an endomorphism of a finite-dimensional space, including $χ_{T} = 1$ in dimension zero).

[L4]

$μ_{T} ∣ χ_{T}$ for every endomorphism $T$ of a finite-dimensional vector space (The minimal polynomial divides the characteristic polynomial, $μ_{T} ∣ χ_{T}$ ).

[L5]

An endomorphism $T$ of a finite-dimensional vector space has a cyclic vector if and only if $μ_{T} = χ_{T}$ (A cyclic vector exists exactly when the minimal and characteristic polynomials agree); $v$ is a cyclic vector when $Z (v; T) = {p (T) v : p \in F [x]}$ is all of $V$ (Cyclic subspaces, cyclic vectors, and vector annihilators).

[L6]

For a finite Galois extension $K / F$ with $G = Gal (K / F)$ one has $∣ G ∣ = [K : F]$ (Equivalent characterizations of a finite Galois extension, Finite Galois extensions and $Gal (K / F)$ , The degree $[K : F] = \dim_{F} K$ of a finite field extension).

[L7]

With $m_{T, v}$ the unique monic generator of ${Ann}_{T} (v) = {p : p (T) v = 0}$ (The vector annihilator is the unique monic generator of ${Ann}_{T} (v)$ and divides the minimal polynomial) and $d = \deg m_{T, v}$ , the list $(v, T v, \dots, T^{d - 1} v)$ is an ordered basis of $Z (v; T)$ (A vector annihilator gives a power basis and its companion matrix).

Proof

technique · direct

1.1L2given

$T^{n} = {i d}_{K}$ , because $σ$ has order $n$ in $Gal (K / F)$ ; so the polynomial $x^{n} - 1$ lies in $Ann (T)$ and $μ_{T} ∣ x^{n} - 1$ by [L2]. In particular $\deg μ_{T} \leq n$ .

1.2L1given

The maps $i d, σ, σ^{2}, \dots, σ^{n - 1}$ are pairwise distinct elements of $Gal (K / F)$ , and their restrictions to $K^{\times}$ are pairwise distinct group homomorphisms $K^{\times} \to K^{\times}$ , since two field automorphisms of $K$ agreeing on $K^{\times}$ agree on $K$ .

2.1step 1.2L1L2

If $p = \sum_{i < n} a_{i} x^{i}$ with $a_{i} \in F$ satisfies $p (T) = 0$ , then $\sum_{i < n} a_{i} σ^{i}$ is the zero function on $K$ , hence on $K^{\times}$ , so [L1] applied to the family of step 1.2 forces every $a_{i}$ to be $0$ ; thus no nonzero polynomial of degree less than $n$ annihilates $T$ , and $\deg μ_{T} \geq n$ .

3.1step 1.1step 2.1L2algebra

Combining steps 1.1 and 2.1, $\deg μ_{T} = n$ , and since $μ_{T}$ is monic and divides the monic $x^{n} - 1$ of the same degree, $μ_{T} = x^{n} - 1$ .

4.1step 3.1L3L4given

By [L3] the polynomial $χ_{T}$ is monic of degree $\dim_{F} K = n$ , and $μ_{T} ∣ χ_{T}$ by [L4]; two monic polynomials of the same degree, one dividing the other, are equal, so $μ_{T} = χ_{T}$ .

5.1step 4.1L5

By [L5] there is a cyclic vector $α \in K$ for $T$ , that is $Z (α; T) = K$ .

6.1step 5.1L6L7given

Let $d = \deg m_{T, α}$ . By [L7] the list $(α, T α, \dots, T^{d - 1} α)$ is an ordered basis of $Z (α; T) = K$ , which has dimension $n$ , so $d = n$ and $(α, σ α, \dots, σ^{n - 1} α)$ is an ordered $F$ -basis of $K$ .

7.1step 1.2step 6.1given∎

Since $Gal (K / F) = {i d, σ, \dots, σ^{n - 1}}$ , that list is exactly the family of conjugates of $α$ , so it is a normal basis.

Remarks

Why the minimal polynomial is forced to be $x^{n} - 1$ . The divisibility $μ_{T} ∣ x^{n} - 1$ is cheap; the content is the lower bound on its degree, and that is exactly Dedekind's independence of characters. Without it the minimal polynomial could be a proper divisor of $x^{n} - 1$ and no cyclic vector would be available.
The hypothesis is on the group, not on the base field. No finiteness or infiniteness of $F$ is used, so this proof also covers cyclic extensions of infinite fields, for which Every finite Galois extension of an infinite field has a normal basis gives a second and quite different argument.

Every finite cyclic extension has a normal basis

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources