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.

Universal property of adjoining a root of an irreducible polynomial

Statement

Let $p \in F [x]$ be monic and irreducible, let $K = F [x] / (p)$ , and put $a = x + (p)$ . If $L / F$ is a field extension and $b \in L$ satisfies $p (b) = 0$ , there is a unique field homomorphism $φ : K ⟶ L$ that fixes $F$ and sends $a$ to $b$ . Its image is $F [b]$ .

Facts & Assumptions

Given: The fields and roots appearing in the statement.

[F1]

Evaluation gives the unique homomorphism $F [x] \to L$ fixing $F$ and sending $x$ to $b$ (Universal property of $R [x]$ : a coefficient homomorphism and the image of $x$ determine a unique ring homomorphism).

[F2]

A homomorphism $R \to S$ whose kernel contains an ideal $I$ factors uniquely through $R / I$ (A ring homomorphism whose kernel contains a two-sided ideal factors uniquely through the quotient ring).

[F3]

$K$ is a field extension, $p (a) = 0$ , and every element of $K$ is a polynomial in $a$ ( $F [x] / (p)$ for monic irreducible $p$ is a field extension containing the root $x + (p)$ with unique reduced representatives).

Proof

technique · direct

1.1

By [F1], evaluation at $b$ is a homomorphism ${ev}_{b} : F [x] \to L$ fixing $F$ .

2.1

Since $p (b) = 0$ , the ideal $(p)$ lies in $\ker ({ev}_{b})$ ; [F2] therefore gives a unique homomorphism $φ : K \to L$ with $φ (f + (p)) = f (b)$ .

F2step 1.1

3.1

The formula fixes constant classes and sends $a = x + (p)$ to $b$ ; its image is exactly the set $F [b]$ of polynomial values.

F3step 2.1algebra

3.2

Because [F3] makes $K$ a field and $φ (1) = 1$ , its kernel is not all of $K$ and hence is zero; thus $φ$ is a field homomorphism.

F3step 2.1algebra

4.1

Any homomorphism fixing $F$ and sending $a$ to $b$ sends every $f (a)$ to $f (b)$ ; since every element is such an $f (a)$ by [F3], it equals $φ$ .

F3step 3.1∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 52 results over 14 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)