TheoremStatement: Literature-sourcedProof: Literature-sourcedSession-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 root is repeated exactly when it is also a root of the formal derivative

Statement

Let $F\subseteq E$ be a field extension, let $0\ne f\in F[x]$ , and let $a\in E$ be a root of $f$ . Then $a$ is a repeated root of $f$ if and only if $f'(a)=0$ .

Facts & Assumptions

Given: A field extension $F\subseteq E$ , a nonzero polynomial $f\in F[x]$ , and a root $a\in E$ of $f$ .

[L1]

The root $a$ is repeated exactly when $(x-a)^2$ divides the image of $f$ in $E[x]$ (Repeated roots in extension fields and separable polynomials).

[L2]

Formal differentiation is linear and satisfies $(uv)'=u'v+uv'$ and $(x-a)'=1$ (Linearity, power rule, Leibniz rule and the degree bound for the formal derivative).

[L3]

A polynomial over a commutative ring vanishes at $a$ exactly when it is divisible by $x-a$ (Factor theorem over a commutative ring).

Proof

technique · direct

1.1

If $a$ is repeated, [L1] gives $f=(x-a)^2q$ , and [L2] gives $f'=2(x-a)q+(x-a)^2q'$ , so evaluation at $a$ yields $f'(a)=0$ .

givenL1L2L3

1.2

Conversely, [L3] gives $f=(x-a)q$ ; [L2] gives $f'=q+(x-a)q'$ , so $f'(a)=q(a)$ , and the assumption $f'(a)=0$ with [L3] gives $q=(x-a)h$ .

givenL2L3algebra

2.1

Substituting the factorization from step 1.2 gives $f=(x-a)^2h$ , so [L1] makes $a$ repeated; together with step 1.1 this proves the biconditional.

step 1.1step 1.2L1∎

Depends on

Used by

Dependency tree · next 3 levels

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