The root number of a primitive Dirichlet character has modulus $1$

Proved

QRHLittlewood.norm_rootNumber_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 $\varepsilon(\chi)=\tau(\chi)/(i^{a}\sqrt N)$ be the root number in the functional equation of its completed $L$ -function, where $a=0$ for even $\chi$ and $a=1$ for odd $\chi$ . Then

|\varepsilon(\chi)|=1.

Formalization Note The root number is Mathlib's DirichletCharacter.rootNumber, which appears in DirichletCharacter.IsPrimitive.completedLFunction_one_sub.

Preamble

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

open Complex

Formal statement

namespace QRHLittlewood

theorem norm_rootNumber_of_isPrimitive {N : ℕ} [NeZero N] {χ : DirichletCharacter ℂ N}
    (hχ : χ.IsPrimitive) : ‖DirichletCharacter.rootNumber χ‖ = 1 := by sorry

end QRHLittlewood

Source

H. Davenport, Multiplicative Number Theory, 3rd ed., Springer GTM 74, Chapter 9.

View graph

The root number of a primitive Dirichlet character has modulus 111

The root number of a primitive Dirichlet character has modulus $1$