$e(a/q)$ depends only on $a$ modulo $q$

Proved

Vino.e_div_congr

by tabbott · Sep 2, 2026 · Mathlib c5ea003 (Lean v4.30.0)

analytic-number-theorycircle-methodnumber-theory

If $q\ge1$ and $a\equiv b\pmod q$ then

e\!\left(\frac{a}{q}\right)=e\!\left(\frac{b}{q}\right).

Every manipulation of complete or reduced exponential sums modulo $q$ — reindexing residues, replacing a residue by its representative, splitting a modulus by the Chinese remainder theorem — reduces to this statement.

Preamble

import Definitions.Def_CircleMethod_char
open Finset

Formal statement

namespace Vino

theorem e_div_congr {q : ℕ} (hq : 0 < q) {a b : ℤ} (h : (q : ℤ) ∣ (a - b)) :
    CircleMethod.e ((a : ℝ) / (q : ℝ)) = CircleMethod.e ((b : ℝ) / (q : ℝ)) := by sorry

end Vino

Source

R. C. Vaughan, The Hardy-Littlewood Method, 2nd ed., Cambridge Tracts in Mathematics 125, Cambridge University Press, 1997, Section 1.1 (the character e(x) = exp(2*pi*i*x)).

View graph

e(a/q)e(a/q)e(a/q) depends only on aaa modulo qqq

$e(a/q)$ depends only on $a$ modulo $q$