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.
Orthogonality relations for Dirichlet characters modulo q
Statement
Let , and let the sum range over all Dirichlet characters modulo .
- For unit classes ,
- For Dirichlet characters modulo ,
Facts & Assumptions
Given: The finite abelian group .
Dirichlet characters modulo are exactly the one-dimensional complex characters of (Dirichlet characters modulo q, Every irreducible representation of a finite abelian group over a splitting field is one-dimensional).
Irreducible complex characters satisfy (The first orthogonality relation for irreducible complex characters).
For a finite group, the column orthogonality sum is when are conjugate and otherwise (The second orthogonality relation for irreducible complex characters).
The sum of the squares of the irreducible character degrees is (The regular character gives a second proof of the sum-of-squares formula).
Proof
By [L1], every irreducible complex character of has degree , and then [L4] shows that their number is because . Thus the irreducible complex characters of are exactly the Dirichlet characters modulo . Since is abelian, every conjugacy class is a singleton and every centralizer is all of .
Applying [L2] to the character group of gives , which is exactly the second displayed formula because . Applying [L3] to the same irreducible character list and using step 1.1 turns the centralizer size into and conjugacy into literal equality of elements, which yields the first displayed formula.
Depends on
- Dirichlet characters modulo q
- Character values on units are roots of unity
- Every irreducible representation of a finite abelian group over a splitting field is one-dimensional
- The first orthogonality relation for irreducible complex characters
- The second orthogonality relation for irreducible complex characters
- The regular character gives a second proof of the sum-of-squares formula
Used by
- A residue-class indicator from character sums Corollary
- An orthogonality table for Dirichlet characters Example
- Mertens sum for primes in an arithmetic progression Theorem
- Primes in one reduced residue class have Dirichlet density 1 over phi(q) Theorem
- The full product of Dirichlet L-functions has no zero on Re s = 1 Theorem
Dependency tree · two levels
19 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
- Kiran S. Kedlaya, Notes on Analytic Number Theory, Chapter 4, Theorem 4.10 (standard reference, not scraped)
- Andrew V. Sutherland, Number Theory I, Corollary 18.16 (standard reference, not scraped)