Prove2Me

Gauss sum of the principal character: τ(χ0)=μ(q)\tau(\chi_0) = \mu(q)

Proved
Vino.gaussE_principal

by jjosh · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

circle-methoddirichlet-charactersgauss-sumsnumber-theory

The Gauss sum of the principal Dirichlet character modulo qq equals the Möbius function:

τ(χ0)=∑m<qχ0(m) e(m/q)=∑m<q(m,q)=1e(m/q)=cq(1)=μ(q).\tau(\chi_0)=\sum_{m<q}\chi_0(m)\,e(m/q)=\sum_{\substack{m<q\\(m,q)=1}} e(m/q)=c_q(1)=\mu(q).

This is the coefficient of the main term in the major-arc expansion of the von Mangoldt exponential sum: at a reduced fraction b/qb/q one has φ(q)S(b/q,N)=∑χχˉ(b)τ(χ)ψ(N,χˉ)+(copraneutral part)\varphi(q)S(b/q,N)=\sum_\chi\bar\chi(b)\tau(\chi)\psi(N,\bar\chi)+(\text{copraneutral part}), and the χ0\chi_0 summand is μ(q)⋅ψ(N,χ0)\mu(q)\cdot\psi(N,\chi_0).

Preamble
import Mathlib
import Definitions.Def_Vino_dirichlet
import Definitions.Def_Vino_ramanujan
import Mathlib.NumberTheory.DirichletCharacter.Basic
Formal statement
namespace Vino

theorem gaussE_principal (q : ℕ) [NeZero q] :
    gaussE q (1 : DirichletCharacter ℂ q)
      = ((ArithmeticFunction.moebius q : ℤ) : ℂ) := by
  sorry

end Vino
Source
Davenport, Multiplicative Number Theory, Ch. 9

View graph