CorollaryStatement: 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.

Factor theorem over a commutative ring

Statement

Let $R$ be a commutative ring, $a\in R$ , and $f\in R[x]$ . Then $f(a)=0$ if and only if $x-a$ divides $f$ in $R[x]$ .

More precisely, there is a unique $q\in R[x]$ such that $f=q(x-a)+f(a)$ .

Facts & Assumptions

Given: A commutative ring $R$ , an element $a\in R$ , and a polynomial $f\in R[x]$ .

[L1]

Division by the monic polynomial $x-a$ gives unique $q,r$ with $f=q(x-a)+r$ and $r=0$ or $\deg r<1$ (Division by a monic polynomial over a commutative ring).

[L2]

Evaluation at $a$ is the finite coefficient sum defining $f(a)$ (Evaluation and roots of a polynomial in a commutative target ring).

[L3]

Evaluation at $a$ is a unital ring homomorphism and sends $x$ to $a$ (Universal property of $R[x]$ : a coefficient homomorphism and the image of $x$ determine a unique ring homomorphism).

Proof

technique · direct

1.1

If $R$ is the zero ring then $R[x]$ has one element, $f=0=0\cdot(x-a)+f(a)$ , and the conclusion holds with $q=0$ ; this case is separated because $x-a=0$ there, which has no leading coefficient and so is not monic, leaving [L1] inapplicable. Otherwise $1\ne0$ , so $x-a$ is monic of degree one. Apply [L1]; the remainder $r$ is zero or constant, and applying [L3] to $f=q(x-a)+r$ gives $f(a)=q(a)(a-a)+r=r$ , so $f=q(x-a)+f(a)$ .

givenL1L2L3

2.1

If $f(a)=0$ , step 1.1 gives $f=q(x-a)$ ; conversely, if $f=q(x-a)$ , applying [L3] gives $f(a)=q(a)(a-a)=0$ , proving the biconditional.

step 1.1L3algebra∎

Depends on

Used by

Dependency tree · next 3 levels

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

Thomas W. Judson, Abstract Algebra: Theory and Applications, Corollary 17.8 (standard reference, not scraped)
Neil Donaldson, Math 120B Notes, Theorem 23.14 (standard reference, not scraped)