LemmaStatement: 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.

For a finite Galois extension, $(α_{j})$ is a base-field basis exactly when the matrix $(σ_{i} α_{j})$ is invertible

Statement

Let $K / F$ be a finite Galois extension of degree $n$ , list its Galois group as $Gal (K / F) = {σ_{1}, \dots, σ_{n}}$ , and let $α_{1}, \dots, α_{n} \in K$ . Let $A \in M_{n} (K)$ be the matrix with entries

$A_{i j} = σ_{i} (α_{j}) (1 \leq i, j \leq n) .$

Then $(α_{1}, \dots, α_{n})$ is an ordered basis of $K$ as an $F$ -vector space (Basis of a vector space: a linearly independent spanning subset; and ordered basis: an injective finite list whose image is a basis) if and only if $A$ is invertible over $K$ (Invertible matrices and the general linear group ${GL}_{n} (F)$ ).

Facts & Assumptions

Given: A finite Galois extension $K / F$ of degree $n$ with $Gal (K / F) = {σ_{1}, \dots, σ_{n}}$ ; elements $α_{1}, \dots, α_{n} \in K$ ; the matrix $A \in M_{n} (K)$ with $A_{i j} = σ_{i} (α_{j})$ (Finite rectangular matrices over a commutative ring, their entries, rows and columns); and the $F$ -linear map $Φ ⁣ : F^{n} \to K$ given by $Φ (a) = \sum_{j} a_{j} α_{j}$ . Each $σ_{i}$ is an $F$ -automorphism of $K$ (Relative field automorphisms and $Aut (K / F)$ ), hence additive and $F$ -linear.

[L1]

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)$ ); so $\dim_{F} K = n$ (The degree $[K : F] = \dim_{F} K$ of a finite field extension).

[L2]

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).

[L3]

For a linear map $T : V \to W$ of $F$ -vector spaces with $V$ finite-dimensional, $\dim_{F} V = \dim_{F} (\ker T) + \dim_{F} (im T)$ (Rank-nullity: $\dim_{F} V = nullity T + rank T$ ).

[L4]

For $A \in M_{n} (F)$ and $L_{A} (x) = A x$ on $M_{n \times 1} (F)$ : $A$ is invertible if and only if $L_{A}$ is a linear isomorphism (A square matrix is invertible exactly when its multiplication map is a linear isomorphism; matrices preserve inverses of linear isomorphisms).

[L5]

Let $R$ be a commutative ring, $n \geq 1$ , $A \in M_{n} (R)$ . Then $A$ is invertible if and only if $\det (A)$ is a unit of $R$ (A positive-sized square matrix over a commutative ring is invertible if and only if its determinant is a unit).

[L6]

$\det (A^{T}) = \det (A)$ for every $A \in M_{n} (R)$ over a commutative ring (For every square matrix over a commutative ring, $\det (A^{T}) = \det (A)$ ); the transpose is $(A^{T})_{j i} = A_{i j}$ (Entrywise ring-matrix operations, rectangular matrix products, identity matrices and transpose).

Proof

technique · direct

1.1L1L3

By [L1] the $F$ -vector space $K$ has dimension $n$ , and $Φ$ is a map between $F$ -vector spaces of dimension $n$ ; so by [L3] it is injective if and only if it is surjective, and $(α_{1}, \dots, α_{n})$ is an ordered basis of $K$ over $F$ exactly when $Φ$ is bijective.

1.2given

For the implication that a basis has an invertible matrix, suppose $(α_{1}, \dots, α_{n})$ is an ordered basis, and let $c \in K^{n}$ satisfy $A^{T} c = 0$ , that is $\sum_{i} c_{i} σ_{i} (α_{j}) = 0$ for every $j$ . The map $θ ⁣ : K \to K$ , $θ (x) = \sum_{i} c_{i} σ_{i} (x)$ , is $F$ -linear because each $σ_{i}$ is, and it vanishes at every $α_{j}$ , hence on their $F$ -span, which is $K$ .

2.1step 1.1given

For the implication that a non-basis has a singular matrix, suppose $(α_{1}, \dots, α_{n})$ is not an ordered basis. By step 1.1 the map $Φ$ is not injective, so there is $a \in F^{n}$ with $a \neq 0$ and $\sum_{j} a_{j} α_{j} = 0$ . Applying $σ_{i}$ and using $σ_{i} (a_{j}) = a_{j}$ for $a_{j} \in F$ gives $\sum_{j} σ_{i} (α_{j}) a_{j} = 0$ for every $i$ , that is $A a = 0$ with $a \neq 0$ in $K^{n}$ . Were $A$ invertible with inverse $B$ , this would force $a = B (A a) = 0$ ; so $A$ is not invertible.

2.2step 1.2L2

So $\sum_{i} c_{i} σ_{i}$ is the zero function on $K$ , in particular on $K^{\times}$ . The restrictions $σ_{i} ∣_{K^{\times}} ⁣ : K^{\times} \to K^{\times}$ are group homomorphisms and are pairwise distinct, since two automorphisms of $K$ agreeing on $K^{\times}$ agree on $K$ ; so [L2] forces $c_{i} = 0$ for every $i$ .

3.1step 2.2L3L4L5L6

Hence the $K$ -linear map $x \mapsto A^{T} x$ on $K^{n}$ has zero kernel, so by [L3] over $K$ it is also surjective and therefore a linear isomorphism; by [L4] the matrix $A^{T}$ is invertible, so $\det (A^{T})$ is a unit of $K$ by [L5], and $\det (A) = \det (A^{T})$ by [L6] is a unit, whence $A$ is invertible by [L5].

4.1step 2.1step 3.1∎

Step 2.1 gives one implication, that a list which is not a basis has a matrix that is not invertible, and step 3.1 gives the other, that a list which is a basis has an invertible matrix; together they are the stated equivalence.

Remarks

Why the transpose appears. The dependence relation among the $α_{j}$ produces a null vector on the right of $A$ , while the Dedekind relation among the $σ_{i}$ produces one on the right of $A^{T}$ . Only the determinant sees both, which is why the two halves are joined through For every square matrix over a commutative ring, $\det (A^{T}) = \det (A)$ rather than by a single rank computation.
Where the Galois hypothesis is used. Twice: to know that the group has exactly $n = [K : F]$ elements, so that $A$ is square, and to know that the $σ_{i}$ are $F$ -linear, which is what lets step 2.1 pull the scalars $a_{j}$ through.

Depends on

Used by

Dependency tree · two levels

60 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), Lemma 8.23 (standard reference, not scraped)
J. S. Milne, Fields and Galois Theory, v5.10, Corollary 5.16 (standard reference, not scraped)

For a finite Galois extension, (αj)(αj​) is a base-field basis exactly when the matrix (σiαj)(σi​αj​) is invertible