TheoremStatement: Literature-sourcedProof: Literature-sourcedSession-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.

A simple algebraic extension is its minimal-polynomial quotient and has power basis $1, a, \dots, a^{n - 1}$ and degree $n$

Statement

Let $K / F$ be a field extension and let $a \in K$ be algebraic with minimal polynomial $m_{a}$ of degree $n$ . Evaluation induces an $F$ -isomorphism $F [x] / (m_{a}) ≅ F (a), f + (m_{a}) ⟼ f (a) .$ Moreover, every element of $F (a)$ has a unique expression $c_{0} + c_{1} a + \dots + c_{n - 1} a^{n - 1}, c_{j} \in F .$ Thus $1, a, \dots, a^{n - 1}$ is the power basis, and the degree of the simple extension is $[F (a) : F] = n$ .

Facts & Assumptions

Given: A field extension $K / F$ and an algebraic element $a \in K$ whose minimal polynomial $m_{a}$ has degree $n$ .

[F1]

Evaluation has kernel $(m_{a})$ , and $m_{a}$ is irreducible (The evaluation kernel and the unique monic irreducible minimal polynomial of an algebraic element).

[F2]

The first isomorphism theorem identifies a ring modulo the kernel of a homomorphism with its image (First isomorphism theorem for rings: $R / \ker f ≅ im f$ ).

[F3]

Division by a nonzero polynomial gives a unique remainder of smaller degree (Division algorithm for polynomials over a field).

[F4]

A quotient $F [x] / (p)$ by a nonconstant polynomial is a field exactly when $p$ is irreducible (For a nonconstant $p$ in $F [x]$ , the ideal $(p)$ is maximal and $F [x] / (p)$ is a field exactly when $p$ is irreducible).

[F5]

$F [a]$ is the generated subring and $F (a)$ the generated subfield (Field extensions, generated subrings $F [S]$ , generated subfields $F (S)$ , and simple extensions).

Proof

technique · direct

1.1

Evaluation has image $F [a]$ and kernel $(m_{a})$ by [F1]; [F2] therefore induces $F [x] / (m_{a}) ≅ F [a]$ .

F1F2

2.1

Since $m_{a}$ is irreducible, [F4] makes the quotient and hence $F [a]$ a field.

F1F4step 1.1

3.1

The field $F [a]$ contains $F$ and $a$ , while every subfield containing them contains all polynomial values; minimality in [F5] gives $F [a] = F (a)$ .

F5step 2.1

4.1

Division by $m_{a}$ in [F3] gives each quotient class a representative of degree below $n$ , hence gives every element of $F (a)$ a displayed power expression.

F3step 1.1step 3.1

5.1

If two such expressions agree, their difference is a polynomial of degree below $n$ in the kernel $(m_{a})$ ; uniqueness of the remainder in [F3] makes the difference zero coefficientwise.

F1F3step 4.1

6.1

The existence and uniqueness in steps 4.1--5.1 are exactly the assertion that the displayed powers form a basis; by definition, its number $n$ is $[F (a) : F]$ .

step 4.1step 5.1∎

Depends on

Used by

Dependency tree · next 3 levels

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

A simple algebraic extension is its minimal-polynomial quotient and has power basis 1,a,…,an−11,a,…,an−1 and degree nn