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

$F [x] / (p)$ for monic irreducible $p$ is a field extension containing the root $x + (p)$ with unique reduced representatives

Statement

Let $p \in F [x]$ be monic and irreducible, and put $K = F [x] / (p)$ and $a = x + (p)$ . Then $K$ is a field extension of $F$ , $p (a) = 0$ , and every element of $K$ has a unique representative $r$ with $\deg r < \deg p$ (with $r = 0$ allowed). In particular, if $\deg p = n$ , every element is uniquely $c_{0} + c_{1} a + \dots + c_{n - 1} a^{n - 1}, c_{j} \in F .$

Facts & Assumptions

Given: A field $F$ and a monic irreducible polynomial $p \in F [x]$ .

[F1]

For nonconstant $p \in F [x]$ , the quotient $F [x] / (p)$ is a field if and only if $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).

[F2]

If $g \neq 0$ in $F [x]$ , each $f \in F [x]$ has unique $q, r$ with $f = q g + r$ and either $r = 0$ or $\deg r < \deg g$ (Division algorithm for polynomials over a field).

[F3]

Evaluation at an element is the unique homomorphism extending the coefficient map and sending $x$ to that element (Universal property of $R [x]$ : a coefficient homomorphism and the image of $x$ determine a unique ring homomorphism).

[F4]

A field extension identifies the base field with an injectively embedded subfield (Field extensions, generated subrings $F [S]$ , generated subfields $F (S)$ , and simple extensions).

Proof

technique · direct

1.1

Irreducibility makes $p$ nonconstant, and [F1] makes $K$ a field.

1.2

The constant-class map $F \to K$ is injective: if a constant $c$ lies in $(p)$ , then $c = q p$ ; uniqueness in [F2], comparing $c = 0 p + c$ with $c = q p + 0$ , forces $c = 0$ .

1.3

In $K$ , $p (a) = p (x) + (p) = 0$ by the quotient arithmetic; equivalently this is evaluation at $a$ from [F3].

F3algebra

1.4

By [F2], write $f = q p + r$ with $r = 0$ or $\deg r < \deg p$ ; hence $f + (p) = r + (p)$ , so every class has a reduced representative.

2.1

Thus the constant-class map supplies the field extension $K / F$ .

F4step 1.1step 1.2

2.2

If two reduced representatives $r, s$ give the same class, then $r - s = q p$ . Applying uniqueness in [F2] to $r - s$ shows $q = 0$ and $r = s$ .

F2step 1.4

3.1

Writing the unique reduced polynomial coefficientwise yields the displayed unique expression; when $n = 1$ it consists only of $c_{0}$ , and the zero class is represented by the zero polynomial.

step 1.4step 2.2algebra∎

Depends on

Used by

Dependency tree · next 3 levels

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

T. Judson, Abstract Algebra: Theory and Applications, Extension Fields (standard reference, not scraped)

F[x]/(p)F[x]/(p) for monic irreducible pp is a field extension containing the root x+(p)x+(p) with unique reduced representatives