Alphabeta MathHow 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.
Euler product for Dirichlet L-functions
Statement
For every Dirichlet character and every with ,
and this product is nonzero on .
Facts & Assumptions
Given: A Dirichlet character and a complex number with .
The Dirichlet -function is (Dirichlet L-functions).
A completely multiplicative arithmetic function has the geometric Euler product at points of absolute convergence (Completely multiplicative Dirichlet series have geometric Euler factors).
Proof
A Dirichlet character is completely multiplicative on , because it is multiplicative on unit classes and both sides vanish when a nonunit factor is present. Hence [L2] applied to and [L1] give the Euler product formula on .
Write . Then , so converges. Therefore converges absolutely, and is the absolutely convergent local series. Summing over shows that the Euler product of step 1.1 is the exponential of a convergent complex series, so it cannot vanish.
Depends on
Used by
- A real nonprincipal Dirichlet L-function is nonzero at one Lemma
- Dirichlet character chebyshev laplace transform Lemma
- Finite Euler factors under character induction 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
- The principal Dirichlet L-function factors through zeta Theorem
Dependency tree · two levels
6 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, Definition 3.4 (standard reference, not scraped)
- Andrew V. Sutherland, Number Theory I, Definition 18.19 (standard reference, not scraped)