TheoremStatement: Literature-sourcedProof: Literature-sourcedprecheck 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 \neq 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 $(u v)^{'} = u^{'} v + u v^{'}$ 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)^{2} q$ , and [L2] gives $f^{'} = 2 (x - a) q + (x - a)^{2} q^{'}$ , 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)^{2} h$ , 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 · two levels

9 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

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