TheoremStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-13

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.

Two simple transcendental extensions are uniquely $F$ -isomorphic once their generators are matched

Statement

Let $a$ and $b$ be transcendental over $F$ . There is a unique $F$ -isomorphism $Φ : F (a) ⟶ F (b)$ such that $Φ (a) = b$ .

Facts & Assumptions

Given: Transcendental elements $a$ and $b$ over the same field $F$ .

[F1]

Every element of $F (a)$ has the form $f (a) g (a)^{- 1}$ with $f, g \in F [x]$ and $g \neq 0$ , and likewise for $F (b)$ (A simple transcendental extension consists exactly of rational expressions in its generator).

[A1]

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

Proof

technique · direct

1.1

Define $Φ (f (a) g (a)^{- 1}) = f (b) g (b)^{- 1}$ . The denominators are nonzero by [A1].

A1F1

2.1

If $f (a) g (a)^{- 1} = r (a) s (a)^{- 1}$ , cross-multiplication gives $(f s - r g) (a) = 0$ ; [A1] gives $f s = r g$ , and evaluation at $b$ proves that the two proposed images agree. Thus $Φ$ is well-defined.

A1step 1.1algebra

2.2

The formula preserves sums and products, fixes $F$ , and sends $a$ to $b$ .

step 1.1algebra

3.1

The same construction with $a$ and $b$ interchanged is inverse to $Φ$ , so $Φ$ is an $F$ -isomorphism.

A1F1step 2.1step 2.2

4.1

Any $F$ -homomorphism sending $a$ to $b$ must send $f (a) g (a)^{- 1}$ to $f (b) g (b)^{- 1}$ ; [F1] therefore forces it to equal $Φ$ .

F1step 1.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 13 results over 6 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

J. S. Milne, Fields and Galois Theory (standard reference, not scraped)

Two simple transcendental extensions are uniquely FF-isomorphic once their generators are matched