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

One element of a transcendence basis can be exchanged for a suitable rival

Statement

Let k⊆K be a field extension, let S and T be transcendence bases of K over k, and let s∈S. Then there exists t∈T such that (T∖{t})∪{s} is again a transcendence basis of K over k.

Facts & Assumptions

Given: A field extension k⊆K, transcendence bases S and T of K over k, and an element s∈S.

[L1]

If a subset of K is algebraically independent and K is algebraic over the field it generates, then that subset is a transcendence basis (A maximal algebraically independent set is a transcendence basis).

Proof

technique · direct
1.1givenchoose

Because T is a transcendence basis, K is algebraic over k(T); in particular s is algebraic over k(T). Choose a finite subset U={t1,…,tm}⊆T of minimal size such that s is algebraic over k(U).

2.1step 1.1algebra

Minimality forces m≥1. Choose a nonzero polynomial relation for s over k(U) and clear denominators to obtain P(s,t1,…,tm)=0 with P∈k[X,Y1,…,Ym] nonzero. The variable Ym must occur in P; otherwise the same relation would show that s is algebraic over k(t1,…,tm−1), contradicting minimality of U. Therefore, viewing P as a polynomial in Ym over k(s,t1,…,tm−1), we see that tm is algebraic over k(s,t1,…,tm−1).

3.1step 2.1given

Put T′=(T∖{tm})∪{s}. If T′ were algebraically dependent, then s would be algebraic over k(T∖{tm}). Together with step 2.1 this would make tm algebraic over k(T∖{tm}), contradicting algebraic independence of T. Hence T′ is algebraically independent.

4.1L1step 3.1algebra∎

Step 2.1 shows that tm is algebraic over k(T′), so k(T) is algebraic over k(T′). Since K is algebraic over k(T), it is also algebraic over k(T′). By [L1], T′ is a transcendence basis of K over k.

Depends on

Used by

Dependency tree · two levels

3 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