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.
For , the sum of all -th roots of unity is zero
Statement
For with , the sum of all th roots of unity is . The conventions and prerequisite facts used below are recorded in The -th roots of a complex number and the distinct roots of unity for every , The complex numbers form a field, and every nonzero has inverse , Integer powers in the complex field, The product of a finite list in a monoid, by recursion, with the empty product () equal to the identity, Generalised associativity: in a monoid the product of a finite list does not depend on the bracketing, and in a commutative monoid it does not depend on the order of the factors either.
Facts & Assumptions
Given: A natural and , with as in The -th roots of a complex number and the distinct roots of unity for every .
Proof
The roots are the distinct list , with and .
The cyclic successor map on the initial segment is a permutation; the commutative-monoid permutation rule therefore gives for .
Thus , and field cancellation gives .
Depends on
- The $n$-th roots of a complex number and the $n$ distinct roots of unity for every $n\ge1$
- The complex numbers form a field, and every nonzero $x+iy$ has inverse $(x-iy)/(x^2+y^2)$
- Integer powers in the complex field
- The product $g_0 g_1 \cdots g_{n-1}$ of a finite list in a monoid, by recursion, with the empty product ($n = 0$) equal to the identity
- Generalised associativity: in a monoid the product of a finite list does not depend on the bracketing, and in a commutative monoid it does not depend on the order of the factors either
Used by
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 82 results over 20 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
- J. Lebl, Basic Analysis I: Complex Numbers and the Complex Exponential (standard reference, not scraped)