$|\tau(\chi)|^2=N$ for primitive Dirichlet characters

Proved

QRHLittlewood.normSq_gaussSum_of_isPrimitive

by @bwdaugherty · Oct 16, 2026 · Mathlib 0df444a (Lean v4.33.1)

analytic-number-theorynumber-theory

Let $\chi$ be a primitive Dirichlet character modulo $N\ge1$ and let

\tau(\chi)=\sum_{a\in\mathbb Z/N\mathbb Z}\chi(a)\,e^{2\pi i a/N}

be its Gauss sum with respect to the standard additive character. Then

|\tau(\chi)|^2=N.

This holds for every modulus, prime or composite. It gives $|\tau(\chi)|=\sqrt N$ and hence the unit modulus of the root number in the functional equation of $L(s,\chi)$ .

Formalization Note The Gauss sum is Mathlib's gaussSum χ ZMod.stdAddChar and primitivity is DirichletCharacter.IsPrimitive.

Preamble

import Mathlib.NumberTheory.LSeries.DirichletContinuation
import Mathlib.NumberTheory.DirichletCharacter.GaussSum
import Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar

open Complex

Formal statement

namespace QRHLittlewood

theorem normSq_gaussSum_of_isPrimitive {N : ℕ} [NeZero N] {χ : DirichletCharacter ℂ N}
    (hχ : χ.IsPrimitive) : Complex.normSq (gaussSum χ ZMod.stdAddChar) = N := by sorry

end QRHLittlewood

Source

H. Davenport, Multiplicative Number Theory, 3rd ed., Springer GTM 74, Chapter 9 (Gauss sums for primitive characters).

View graph

∣τ(χ)∣2=N|\tau(\chi)|^2=N∣τ(χ)∣2=N for primitive Dirichlet characters

$|\tau(\chi)|^2=N$ for primitive Dirichlet characters