LemmaStatement: Literature-sourcedProof: Literature-sourcedprecheck 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.

Over an infinite base field, no nonzero polynomial vanishes at the conjugate tuple of every element

Statement

Let $K / F$ be a finite Galois extension of degree $n$ whose base field $F$ is infinite, and list $Gal (K / F) = {σ_{1}, \dots, σ_{n}}$ . Then for every nonzero $f \in K [x_{1}, \dots, x_{n}]$ (Polynomial rings in finitely many commuting indeterminates by iteration) there exists $α \in K$ with

$f (σ_{1} α, \dots, σ_{n} α) \neq 0.$

Facts & Assumptions

Given: A finite Galois extension $K / F$ of degree $n$ with $F$ infinite and $Gal (K / F) = {σ_{1}, \dots, σ_{n}}$ ; by [L4] the $F$ -vector space $K$ has dimension $n$ , so an ordered $F$ -basis $(α_{1}, \dots, α_{n})$ of $K$ exists (Basis of a vector space: a linearly independent spanning subset; and ordered basis: an injective finite list whose image is a basis).

[L1]

Let $S$ be an integral domain and $R \subseteq S$ an infinite subring. If $g \in S [x_{1}, \dots, x_{m}]$ satisfies $g (a_{1}, \dots, a_{m}) = 0$ for all $a_{1}, \dots, a_{m} \in R$ , then $g = 0$ (A polynomial vanishing at every tuple from an infinite subdomain is the zero polynomial).

[L2]

For a finite Galois extension $K / F$ of degree $n$ with $Gal (K / F) = {σ_{1}, \dots, σ_{n}}$ and $α_{1}, \dots, α_{n} \in K$ , the list $(α_{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]

For commutative rings $R, S$ , a unital ring homomorphism $φ ⁣ : R \to S$ and $s \in S$ , there is a unique unital ring homomorphism $R [x] \to S$ extending $φ$ on constants and sending $x$ to $s$ (Universal property of $R [x]$ : a coefficient homomorphism and the image of $x$ determine a unique ring homomorphism). Iterating this along Polynomial rings in finitely many commuting indeterminates by iteration gives, for any commutative $K$ -algebra $T$ and any $t_{1}, \dots, t_{n} \in T$ , a unique $K$ -algebra homomorphism $K [x_{1}, \dots, x_{n}] \to T$ sending $x_{i}$ to $t_{i}$ .

[L4]

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

[L5]

$A \in M_{n} (K)$ is invertible when some $B \in M_{n} (K)$ satisfies $A B = I_{n} = B A$ ; such a $B$ is unique and written $A^{- 1}$ (Invertible matrices and the general linear group ${GL}_{n} (F)$ , Entrywise ring-matrix operations, rectangular matrix products, identity matrices and transpose).

Proof

technique · contrapositive

1.1contrapositive-reduceassume-hyp

It suffices to prove the contrapositive: if $f \in K [x_{1}, \dots, x_{n}]$ satisfies $f (σ_{1} α, \dots, σ_{n} α) = 0$ for every $α \in K$ , then $f = 0$ . Assume that hypothesis on $f$ .

1.2L2L4L5given

Fix an ordered $F$ -basis $(α_{1}, \dots, α_{n})$ of $K$ and put $A_{i j} = σ_{i} (α_{j})$ ; by [L2] the matrix $A$ is invertible, with inverse $A^{- 1}$ as in [L5].

2.1step 1.2given

For $c \in F^{n}$ write $α (c) : = \sum_{j} c_{j} α_{j}$ ; then $c \mapsto α (c)$ is a bijection $F^{n} \to K$ because the $α_{j}$ form a basis, and $σ_{i} (α (c)) = \sum_{j} c_{j} σ_{i} (α_{j}) = (A c)_{i}$ since each $σ_{i}$ fixes $F$ pointwise and is additive.

2.2step 1.2L3

Let $ψ ⁣ : K [x_{1}, \dots, x_{n}] \to K [x_{1}, \dots, x_{n}]$ be the unique $K$ -algebra homomorphism with $ψ (x_{i}) = \sum_{j} A_{i j} x_{j}$ , and $ψ^{'}$ the unique one with $ψ^{'} (x_{i}) = \sum_{j} (A^{- 1})_{i j} x_{j}$ ; both exist by [L3].

3.1step 1.1step 2.1step 2.2L3

For $c \in F^{n}$ , the evaluation homomorphism $K [x_{1}, \dots, x_{n}] \to K$ at $c$ composed with $ψ$ sends $x_{i}$ to $\sum_{j} A_{i j} c_{j} = (A c)_{i}$ , so by the uniqueness clause of [L3] it is evaluation at $A c$ ; hence $ψ (f)$ evaluated at $c$ equals $f (A c) = f (σ_{1} α (c), \dots, σ_{n} α (c))$ , which is $0$ by the hypothesis of step 1.1.

4.1step 3.1L1given

So $ψ (f)$ vanishes at every tuple from the infinite subring $F$ of the integral domain $K$ , and [L1] gives $ψ (f) = 0$ .

5.1step 2.2step 4.1L3L5discharge-contrapositive∎

The composite $ψ^{'} \circ ψ$ is a $K$ -algebra endomorphism sending $x_{i}$ to $\sum_{j} A_{i j} \sum_{k} (A^{- 1})_{j k} x_{k} = \sum_{k} (A A^{- 1})_{i k} x_{k} = x_{i}$ , so it is the identity by the uniqueness clause of [L3]; applying $ψ^{'}$ to step 4.1 therefore gives $f = ψ^{'} (ψ (f)) = ψ^{'} (0) = 0$ , which is the contrapositive.

Remarks

Where infiniteness of $F$ enters. Only in step 4.1, through [L1]. Over a finite base field the conclusion is false: with $∣ F ∣ = q$ and $n = [K : F]$ , the nonzero polynomial $x_{1}^{q^{n}} - x_{1}$ vanishes at every conjugate tuple, since every element of $K$ satisfies $x^{q^{n}} = x$ . The finite case of the normal basis theorem is therefore proved by a different argument (Every finite cyclic extension has a normal basis).

Depends on

Used by

Every finite Galois extension of an infinite field has a normal basis Theorem

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

P. L. Clark, Field Theory (course notes/monograph), Theorem 8.24 (standard reference, not scraped)
J. S. Milne, Fields and Galois Theory, v5.10, Lemma 5.19 and the normal basis theorem (standard reference, not scraped)