DefinitionDefinition: AI-adaptedProof: Not applicableaudited 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.

Repeated roots in extension fields and separable polynomials

Definition

Let $F$ be a field, let $E$ be an extension field in which $F$ is a subfield (Subfield: a subring of a field closed under inverses of its nonzero elements, and therefore a field with the restricted operations), and let $0 \neq f \in F [x]$ . The coefficient inclusion induces a homomorphism $F [x] \to E [x]$ by the universal property (Universal property of $R [x]$ : a coefficient homomorphism and the image of $x$ determine a unique ring homomorphism).

An element $a \in E$ is a repeated root of $f$ in $E$ when $(x - a)^{2}$ divides the image of $f$ in $E [x]$ . It is a root in the ordinary sense of Evaluation and roots of a polynomial in a commutative target ring, and Factor theorem over a commutative ring identifies divisibility by $x - a$ with vanishing at $a$ .

The polynomial $f$ is separable over $F$ when it has no repeated root in any extension field of $F$ . A nonzero constant polynomial is therefore separable. The zero polynomial is not called separable under this convention.

Depends on

Dependency tree · 2 levels

Sources

Brian Conrad, Differential Criterion and Primitivity, Section 1