Reduced residues as the unit group of $\mathbb Z/q$

Proved

Vino.sum_coprime_eq_sum_units

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

algebraanalytic-number-theorynumber-theoryramanujan-sums

Let $q\ge1$ and let $f:\mathbb Z/q\mathbb Z\to\mathbb C$ . Then

\sum_{\substack{a<q\\ (a,q)=1}}f(a\bmod q)\;=\;\sum_{u\in(\mathbb Z/q\mathbb Z)^{\times}}f(u).

The reduction of the sum over reduced residues to a sum over the unit group is what makes group-theoretic reindexing available: multiplying by a fixed unit, or splitting the group by the Chinese remainder theorem, are then bijections of the index set rather than delicate statements about representatives.

Preamble

import Definitions.Def_Vino_ramanujan
import Mathlib.Data.ZMod.Units
open Finset

Formal statement

namespace Vino

theorem sum_coprime_eq_sum_units {q : ℕ} [NeZero q] (f : ZMod q → ℂ) :
    ∑ a ∈ (Finset.range q).filter (fun a => Nat.Coprime a q), f ((a : ℕ) : ZMod q)
      = ∑ u : (ZMod q)ˣ, f (u : ZMod 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 2.6 and Chapter 3; G. H. Hardy and E. M. Wright, An Introduction to the Theory of Numbers, 6th ed., Oxford University Press, 2008, Section 16.6 (Ramanujan's sum c_q(n)).

View graph

Reduced residues as the unit group of Z/q\mathbb Z/qZ/q

Reduced residues as the unit group of $\mathbb Z/q$