TheoremStatement: Literature-sourcedProof: Literature-sourcedSession-authored (Fable 5 assisted)precheck 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 Galois extension of an infinite field has a normal basis

Statement

Let $K / F$ be a finite Galois extension whose base field $F$ is infinite. Then $K / F$ has a normal basis (Normal bases of a finite Galois extension): there is $α \in K$ such that $(σ_{1} α, \dots, σ_{n} α)$ is an ordered $F$ -basis of $K$ , where $Gal (K / F) = {σ_{1}, \dots, σ_{n}}$ .

Facts & Assumptions

Given: A finite Galois extension $K / F$ (Finite Galois extensions and $Gal (K / F)$ ) of degree $n$ with $F$ infinite, and $Gal (K / F) = {σ_{1}, \dots, σ_{n}}$ numbered so that $σ_{1} = {i d}_{K}$ ; the matrix $B$ over $K [x_{1}, \dots, x_{n}]$ with $B_{i j} : = x_{k}$ where $k$ is the index determined by $σ_{i} σ_{j} = σ_{k}$ ; and $D : = \det B$ (For $n \geq 1$ , the determinant over a commutative ring by the Leibniz formula, and $∣ \det A ∣$ for a real matrix).

[L1]

For every nonzero $f \in K [x_{1}, \dots, x_{n}]$ there is $α \in K$ with $f (σ_{1} α, \dots, σ_{n} α) \neq 0$ (Over an infinite base field, no nonzero polynomial vanishes at the conjugate tuple of every element).

[L2]

$(α_{1}, \dots, α_{n})$ is an ordered $F$ -basis of $K$ if and only if the matrix $A$ with $A_{i j} = σ_{i} (α_{j})$ is invertible (For a finite Galois extension, $(α_{j})$ is a base-field basis exactly when the matrix $(σ_{i} α_{j})$ is invertible).

[L3]

$\det (A) = \sum_{σ \in S_{n}} sgn (σ) \prod_{i} a_{σ (i), i}$ (For $n \geq 1$ , the determinant over a commutative ring by the Leibniz formula, and $∣ \det A ∣$ for a real matrix); a matrix over a commutative ring is invertible if and only if its determinant is a unit (A positive-sized square matrix over a commutative ring is invertible if and only if its determinant is a unit).

[L4]

A matrix $A$ is invertible when some $B$ satisfies $A B = I_{n} = B A$ (Invertible matrices and the general linear group ${GL}_{n} (F)$ ); matrix products, the identity and the transpose are as in Entrywise ring-matrix operations, rectangular matrix products, identity matrices and transpose, and obey the arithmetic laws of Matrix arithmetic over a commutative ring is associative, unital and distributive, and transpose reverses products.

[L5]

$K [x_{1}, \dots, x_{n}]$ is an integral domain (A polynomial ring in finitely many indeterminates over an integral domain is an integral domain, Polynomial rings in finitely many commuting indeterminates by iteration), and for any commutative $K$ -algebra $T$ and $t_{1}, \dots, t_{n} \in T$ there is a unique $K$ -algebra homomorphism $K [x_{1}, \dots, x_{n}] \to T$ with $x_{i} \mapsto t_{i}$ (Universal property of $R [x]$ : a coefficient homomorphism and the image of $x$ determine a unique ring homomorphism).

Proof

technique · direct

1.1

$B$ is a well-defined $n \times n$ matrix over $K [x_{1}, \dots, x_{n}]$ : for each pair $(i, j)$ the product $σ_{i} σ_{j}$ lies in the group $Gal (K / F)$ and so equals $σ_{k}$ for exactly one index $k$ .

given

2.1

Let $ε ⁣ : K [x_{1}, \dots, x_{n}] \to K$ be the $K$ -algebra homomorphism with $ε (x_{1}) = 1$ and $ε (x_{k}) = 0$ for $k \neq 1$ , supplied by [L5]. Applying $ε$ entrywise to $B$ gives the matrix $P \in M_{n} (K)$ with $P_{i j} = 1$ when $σ_{i} σ_{j} = σ_{1} = i d$ , that is when $σ_{j} = σ_{i}^{- 1}$ , and $P_{i j} = 0$ otherwise.

step 1.1L5given

3.1

$P$ is invertible, with $P^{T}$ as an inverse: the $(i, i^{'})$ entry of $P P^{T}$ is $\sum_{j} P_{i j} P_{i^{'} j}$ , and a term is nonzero exactly when $σ_{j} = σ_{i}^{- 1}$ and $σ_{j} = σ_{i^{'}}^{- 1}$ , which happens for exactly one $j$ when $i = i^{'}$ and for no $j$ otherwise; so $P P^{T} = I_{n}$ , and the same computation on $P^{T} P$ gives $I_{n}$ . Hence $\det P$ is a unit of $K$ by [L3], and in particular $\det P \neq 0$ .

step 2.1L3L4

4.1

Since $\det$ is a polynomial expression in the entries by [L3] and $ε$ is a ring homomorphism, $ε (D) = ε (\det B) = \det P \neq 0$ ; hence $D \neq 0$ in $K [x_{1}, \dots, x_{n}]$ .

step 2.1step 3.1L3L5

5.1

By [L1] there is $α \in K$ with $D (σ_{1} α, \dots, σ_{n} α) \neq 0$ . Substituting $x_{k} \mapsto σ_{k} (α)$ in $B$ replaces the entry $B_{i j} = x_{k}$ , where $σ_{i} σ_{j} = σ_{k}$ , by $σ_{k} (α) = σ_{i} (σ_{j} (α))$ ; since substitution is a ring homomorphism, it carries $D = \det B$ to the determinant of the matrix $A$ with $A_{i j} = σ_{i} (α_{j})$ for $α_{j} : = σ_{j} (α)$ . So $\det A \neq 0$ .

step 4.1L1L3L5

6.1

A nonzero element of the field $K$ is a unit, so $A$ is invertible by [L3], and [L2] makes $(α_{1}, \dots, α_{n}) = (σ_{1} α, \dots, σ_{n} α)$ an ordered $F$ -basis of $K$ ; that is a normal basis.

step 5.1L2L3∎

Remarks

What the specialisation is for. The matrix of indeterminates is a device for showing that one determinant polynomial is not the zero polynomial, and the cheapest way to see that is to send it to a permutation matrix. Nothing about the particular substitution $x_{1} \mapsto 1$ survives into the conclusion: the element $α$ produced in step 5.1 has no relation to it.
Why $σ_{1}$ is the identity. Only so that the specialised matrix is the permutation matrix of $σ \mapsto σ^{- 1}$ ; any other choice of which indeterminate to set to $1$ would give the permutation matrix of a different bijection, with the same conclusion.

Depends on

Used by

Dependency tree · two levels

48 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

P. L. Clark, Field Theory (course notes/monograph), Theorem 8.25 (standard reference, not scraped)
K. Conrad, Linear Independence of Characters (expository blurb), Theorem 3.6 (standard reference, not scraped)