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.

A polynomial vanishing at every tuple from an infinite subdomain is the zero polynomial

Statement

Let $S$ be an integral domain, let $R \subseteq S$ be a subring whose underlying set is infinite, let $m \geq 1$ , and let $f \in S [x_{1}, \dots, x_{m}]$ (Polynomial rings in finitely many commuting indeterminates by iteration). If

$f (a_{1}, \dots, a_{m}) = 0 for all a_{1}, \dots, a_{m} \in R,$

then $f = 0$ in $S [x_{1}, \dots, x_{m}]$ .

Here $f (a_{1}, \dots, a_{m})$ is the iterated evaluation of Evaluation and roots of a polynomial in a commutative target ring, carried out one indeterminate at a time along the construction of $S [x_{1}, \dots, x_{m}]$ .

Facts & Assumptions

Given: An integral domain $S$ , an infinite subring $R \subseteq S$ , and the polynomial rings $S [x_{1}, \dots, x_{m}]$ built by iteration (Polynomial rings in finitely many commuting indeterminates by iteration).

[L1]

A nonzero polynomial $g \in D [x]$ of degree $k$ over an integral domain $D$ has at most $k$ distinct roots in $D$ (A nonzero polynomial of degree $n$ over an integral domain has at most $n$ distinct roots).

[L2]

If $R$ is an integral domain, then $R [x_{1}, \dots, x_{n}]$ is an integral domain for every $n \in N$ , including $n = 0$ (A polynomial ring in finitely many indeterminates over an integral domain is an integral domain).

[L3]

A nonzero $g = \sum_{i} a_{i} x^{i}$ has a largest index with $a_{i} \neq 0$ , its degree; the zero polynomial has no degree (Degree, leading coefficient and monic polynomial, with the zero polynomial having no degree).

Proof

technique · induction

1.1L1L3base

Base case $m = 1$ : let $g \in S [x]$ vanish at every element of $R$ . If $g \neq 0$ it has a degree $k$ by [L3], so by [L1] it has at most $k$ distinct roots in $S$ ; but every one of the infinitely many elements of $R \subseteq S$ is a root, and an infinite set has more than $k$ elements. Hence $g = 0$ .

1.2ih

Inductive hypothesis: fix $m \geq 1$ and assume that every $g \in S [x_{1}, \dots, x_{m}]$ vanishing at all tuples from $R$ is zero.

2.1step 1.1L2given

Let $f \in S [x_{1}, \dots, x_{m + 1}] = S [x_{1}, \dots, x_{m}] [x_{m + 1}]$ vanish at every tuple from $R$ , and write $f = \sum_{j \leq k} g_{j} x_{m + 1}^{j}$ with $g_{j} \in S [x_{1}, \dots, x_{m}]$ . Fix $a = (a_{1}, \dots, a_{m}) \in R^{m}$ ; then $\sum_{j \leq k} g_{j} (a) x_{m + 1}^{j}$ is an element of $S [x_{m + 1}]$ vanishing at every element of $R$ , so it is zero by step 1.1, and therefore $g_{j} (a) = 0$ for every $j \leq k$ .

3.1step 1.2step 2.1discharge-induction∎

Since $a \in R^{m}$ was arbitrary, each $g_{j}$ vanishes at every tuple from $R$ , so $g_{j} = 0$ by step 1.2 and hence $f = 0$ . This completes the induction, and the statement holds for every $m \geq 1$ .

Remarks

Infinite, not merely large. The hypothesis cannot be weakened to a finite $R$ of any size: over $R = S = F_{q}$ the nonzero polynomial $x^{q} - x$ vanishes at every element, and in $m$ indeterminates so does $x_{1}^{q} - x_{1}$ . This is exactly why the normal basis theorem needs a separate argument over a finite base field (Every finite cyclic extension has a normal basis).

Depends on

Used by

Dependency tree · two levels

13 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.21 (standard reference, not scraped)
J. S. Milne, Fields and Galois Theory, v5.10, Lemma 5.19 (standard reference, not scraped)