TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-16

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 field extension is algebraic

Statement

Every finite field extension $K / F$ is algebraic: each $a \in K$ is a root of a nonzero polynomial in $F [t]$ .

Facts & Assumptions

Given: A finite extension $K / F$ of degree $n$ and an element $a \in K$ .

[L1]

Degree $n$ means that $K$ has an $F$ -basis of size $n$ (The degree $[K : F] = \dim_{F} K$ of a finite field extension).

[L2]

Any $n + 1$ vectors in a space spanned by $n$ vectors are linearly dependent (If $V$ has a spanning set with $n$ elements, then every linearly independent subset of $V$ is finite with at most $n$ elements; in particular $V$ has no linearly independent subset equinumerous with $N$ ).

[L3]

An element is algebraic over $F$ when a nonzero polynomial in $F [t]$ vanishes at it (Algebraic and transcendental elements and algebraic extensions).

Proof

technique · direct

1.1givenL1L2

The $n + 1$ vectors $1, a, \dots, a^{n}$ lie in the $n$ -dimensional $F$ -space $K$ , so [L2] gives coefficients $c_{0}, \dots, c_{n} \in F$ , not all zero, with $\sum_{i = 0}^{n} c_{i} a^{i} = 0$ .

2.1step 1.1L3

The polynomial $p (t) = \sum_{i = 0}^{n} c_{i} t^{i}$ is nonzero and satisfies $p (a) = 0$ , so $a$ is algebraic by [L3].

3.1step 2.1L1∎

Since $a$ was arbitrary, the extension is algebraic. The case $n = 0$ cannot occur for a field extension because $1_{K} \neq 0$ .

Depends on

Dependency tree · 2 levels

Sources

A. W. Knapp, Basic Algebra, 2nd ed., Chapter IX, Section 1