LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-09-04

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 simple residue root determines a coprime residue factorisation

Statement

Let $k$ be a field, let $\overline{f} \in k [T]$ , and let $\overline{a} \in k$ satisfy $\overline{f} (\overline{a}) = 0$ and ${\overline{f}}^{'} (\overline{a}) \neq 0$ . Then there exists $\overline{h} \in k [T]$ such that $\overline{f} = (T - \overline{a}) \overline{h},$ and the factors $T - \overline{a}$ and $\overline{h}$ are coprime.

Facts & Assumptions

Given: A field $k$ , a polynomial $\overline{f} \in k [T]$ , and a simple root $\overline{a}$ of $\overline{f}$ .

[L1]

Polynomial division by a monic linear polynomial is valid over any commutative ring, in particular over a field (The polynomial ring over a commutative ring as finitely supported coefficient sequences with convolution).

Proof

technique · divide by the linear factor and evaluate the derivative

1.1

Since $\overline{f} (\overline{a}) = 0$ , polynomial division by $T - \overline{a}$ gives a factorization $\overline{f} = (T - \overline{a}) \overline{h}$ for some $\overline{h} \in k [T]$ .

L1given

2.1

Differentiating the identity of step 1.1 and evaluating at $\overline{a}$ yields ${\overline{f}}^{'} (\overline{a}) = \overline{h} (\overline{a}) .$ The left side is nonzero by hypothesis, so $\overline{h} (\overline{a}) \neq 0$ . Therefore $T - \overline{a}$ does not divide $\overline{h}$ , which is equivalent to $(T - \overline{a}, \overline{h}) = (1)$ in $k [T]$ .

step 1.1givenalgebra

3.1

Thus a simple residue root determines a coprime residue factorization.

step 1.1step 2.1∎

Depends on

Used by

Factor lifting implies simple-root lifting Corollary

Dependency tree · two levels

11 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

The Stacks Project, Section 10.153: Henselian local rings (standard reference, not scraped)