TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (gpt-5.6-terra)audited 2026-08-27

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 complex polynomial of degree $n$ has exactly $n$ roots counted with multiplicity

Statement

Let $f \in C [x]$ have degree $n \geq 1$ . Then there exist distinct complex numbers $α_{1}, \dots, α_{r}$ and positive integers $m_{1}, \dots, m_{r}$ such that

f (x) = c \prod_{j = 1}^{r} (x - α_{j})^{m_{j}}

for some $c \in C^{\times}$ , with

m_{1} + \dots + m_{r} = n .

These exponents are uniquely determined by $f$ . Equivalently, $f$ has exactly $n$ roots counted with multiplicity.

Facts & Assumptions

Given: A polynomial $f \in C [x]$ of degree $n \geq 1$ .

[L1]

Every nonconstant polynomial in $C [x]$ splits over $C$ (Every nonconstant polynomial in $C [x]$ splits into linear factors).

[L2]

Splitting means a nonzero scalar times a product of linear factors (Polynomials that split and splitting fields of a polynomial or a family of polynomials).

[L3]

The polynomial ring $C [x]$ is a unique factorization domain (For every field $F$ , $F [x]$ is a unique factorisation domain).

Proof

technique · direct

1.1

By [L1] and [L2], there are $c \in C^{\times}$ and complex numbers $β_{1}, \dots, β_{n}$ such that $f (x) = c \prod_{k = 1}^{n} (x - β_{k}) .$ Let $α_{1}, \dots, α_{r}$ be the distinct values among the $β_{k}$ , and let $m_{j}$ be the number of indices $k$ with $β_{k} = α_{j}$ . Then $f (x) = c \prod_{j = 1}^{r} (x - α_{j})^{m_{j}},$ and by construction $m_{1} + \dots + m_{r} = n$ .

L1L2construct

2.1

Suppose also that $f (x) = c^{'} \prod_{j = 1}^{s} (x - γ_{j})^{n_{j}}$ with $c^{'} \in C^{\times}$ , distinct $γ_{j}$ , and positive integers $n_{j}$ . In the UFD $C [x]$ , each linear factor $x - α$ is irreducible, hence prime. Therefore the exponent with which $x - α$ appears in a factorization of $f$ is uniquely determined. After reordering, this gives $r = s, γ_{j} = α_{j}, n_{j} = m_{j} for every j .$ So the multiplicities are well defined.

L3step 1.1algebra

3.1

Step 1.1 gives a factorization whose exponents sum to $n$ , and step 2.1 gives uniqueness of those exponents. This is exactly the statement that a degree- $n$ complex polynomial has exactly $n$ roots counted with multiplicity.

step 1.1step 2.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

12 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

P. L. Clark, Field Theory, Chapters 3 to 5 (standard reference, not scraped)
J. S. Milne, Fields and Galois Theory, v5.10, Chapter 5 (standard reference, not scraped)

A complex polynomial of degree nn has exactly nn roots counted with multiplicity