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.

Algebraicity is transitive in towers of field extensions

Statement

If $F \subseteq K \subseteq L$ , the extension $K / F$ is algebraic, and $L / K$ is algebraic, then $L / F$ is algebraic.

Facts & Assumptions

Given: A tower $F \subseteq K \subseteq L$ with $K / F$ and $L / K$ algebraic, and an element $a \in L$ .

[L1]

Finitely many algebraic generators produce a finite extension (An extension generated by finitely many algebraic elements is finite).

[L2]

An algebraic element generates a finite simple extension (An element is algebraic over $F$ if and only if its simple extension $F (a) / F$ is finite).

[L3]

Finite degrees multiply in a tower (Tower law for finite extensions: $[L : F] = [L : K] [K : F]$ ).

[L4]

Every finite extension is algebraic (Every finite field extension is algebraic).

[L5]

Algebraicity means satisfying a nonzero polynomial over the base (Algebraic and transcendental elements and algebraic extensions).

Proof

technique · direct

1.1givenL5choose

Since $a$ is algebraic over $K$ , choose a nonzero polynomial $c_{0} + c_{1} t + \dots + c_{d} t^{d} \in K [t]$ with value zero at $a$ .

2.1givenstep 1.1L1

Every coefficient $c_{i}$ is algebraic over $F$ . Hence $M = F (c_{0}, \dots, c_{d})$ is finite over $F$ by [L1].

3.1step 1.1step 2.1L2L3

The same polynomial lies in $M [t]$ , so $a$ is algebraic over $M$ and [L2] makes $M (a) / M$ finite. The tower law [L3] makes $M (a) / F$ finite.

4.1step 3.1L4∎

By [L4], $a$ is algebraic over $F$ . Since $a$ was arbitrary, $L / F$ is algebraic.

Depends on

Used by

Dependency tree · two levels

12 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

A. W. Knapp, Basic Algebra, 2nd ed., Chapter IX, Section 1 (standard reference, not scraped)