TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-11

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 nonzero polynomial over a field is separable exactly when its gcd with its derivative is $1$

Statement

Let $F$ be a field and let $0\ne f\in F[x]$ . Then $f$ is separable over $F$ if and only if $\gcd(f,f')=1$ in $F[x]$ .

Facts & Assumptions

Given: A field $F$ and a nonzero polynomial $f\in F[x]$ .

[L1]

In any extension field, a root of $f$ is repeated exactly when it is also a root of $f'$ (A root is repeated exactly when it is also a root of the formal derivative).

[L2]

The monic gcd of two base-field polynomials is unchanged after a field extension (The monic gcd of two base-field polynomials is unchanged after extending the coefficient field).

[L3]

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

[L4]

Every nonzero nonunit polynomial over a field has an irreducible factor (Every nonzero nonunit polynomial over a field factors into irreducible polynomials).

[L5]

A coefficient homomorphism and a chosen image of $x$ determine an evaluation homomorphism (Universal property of $R[x]$ : a coefficient homomorphism and the image of $x$ determine a unique ring homomorphism).

[L6]

The canonical map $R\to R/I$ is a surjective ring homomorphism with kernel $I$ (The canonical projection $R\to R/I$ is a surjective ring homomorphism with kernel $I$ ).

[L7]

For polynomials not both zero over a field, their monic gcd is a polynomial linear combination of them (Bézout identity and the Euclidean algorithm for polynomials over a field).

Proof

technique · direct

1.1

If $\gcd(f,f')=1$ , [L2] says that the gcd remains $1$ in every extension field, and [L7] supplies a Bézout identity there. A common root of $f$ and $f'$ would evaluate that identity to $0=1$ by [L5], so [L1] shows that $f$ has no repeated root and is separable.

givenL1L2L5L7

1.2

Conversely, if $d=\gcd(f,f')\ne1$ , then $d$ is a nonconstant nonunit and [L4] supplies an irreducible factor $p$ of $d$ . Fact [L3] makes $E=F[x]/(p)$ a field. No nonzero constant lies in $(p)$ because a nonconstant polynomial cannot divide it, so [L6] makes the canonical map $F\to E$ injective and identifies $F$ with a subfield of $E$ . Under the evaluation map of [L5], the residue class of $x$ is a common root in $E$ of $p$ , hence of $d$ , $f$ , and $f'$ .

givenL2L3L4L5L6

2.1

By [L1], the common root from step 1.2 is a repeated root of $f$ , so a separable $f$ must have $d=1$ ; combined with step 1.1, this proves the biconditional.

step 1.1step 1.2L1∎

Depends on

Used by

An irreducible polynomial over a field is separable exactly when its derivative is nonzero Corollary

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 73 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

Brian Conrad, Differential Criterion and Primitivity, Proposition 1.2 (standard reference, not scraped)

A nonzero polynomial over a field is separable exactly when its gcd with its derivative is 111