LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-30

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 maximal algebraically independent set is a transcendence basis

Statement

Let $k \subseteq K$ be a field extension, and let $S \subseteq K$ be algebraically independent over $k$ . Assume that $S$ is maximal for inclusion among algebraically independent subsets of $K$ . Then every element of $K$ is algebraic over the generated subfield $k (S)$ , so $S$ is a transcendence basis of $K$ over $k$ .

Facts & Assumptions

Given: A field extension $k \subseteq K$ , a maximal algebraically independent subset $S \subseteq K$ , and the generated subfields $k (S)$ from Field extensions, generated subrings $F [S]$ , generated subfields $F (S)$ , and simple extensions.

[L1]

Evaluation of a polynomial at elements of a commutative target ring is defined coefficientwise; a root is an element where that value is zero (Evaluation and roots of a polynomial in a commutative target ring).

Proof

technique · direct

1.1

Fix $β \in K$ . If $β \in S$ , then $β \in k (S)$ and hence $β$ is algebraic over $k (S)$ because it is a root of $T - β \in k (S) [T]$ .

givenalgebra

1.2

Assume $β \notin S$ . By maximality, $S \cup {β}$ is algebraically dependent over $k$ , so there is a nonzero polynomial $P (T_{1}, \dots, T_{m}, Y) \in k [T_{1}, \dots, T_{m}, Y]$ and elements $s_{1}, \dots, s_{m} \in S$ such that $P (s_{1}, \dots, s_{m}, β) = 0$ . The polynomial $P$ must involve $Y$ , for otherwise $s_{1}, \dots, s_{m}$ would already satisfy a nontrivial polynomial relation over $k$ , contradicting algebraic independence of $S$ .

L1given

2.1

View $P (s_{1}, \dots, s_{m}, Y)$ as a nonzero polynomial in $k [S] [Y]$ and then in $k (S) [Y]$ . After dividing by its leading coefficient in the field $k (S)$ , we obtain a monic polynomial $Q (Y) \in k (S) [Y]$ with $Q (β) = 0$ . Therefore $β$ is algebraic over $k (S)$ .

step 1.2L1algebra

3.1

Steps 1.1 and 2.1 cover every $β \in K$ , so $K / k (S)$ is algebraic. Hence $S$ is a transcendence basis of $K$ over $k$ .

step 1.1step 2.1∎

Depends on

Used by

Dependency tree · two levels

8 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

J. S. Milne, Fields and Galois Theory, v5.10, Proposition 9.12 (standard reference, not scraped)