Ramanujan sums are invariant under unit twists of the argument

Proved

Vino.ramanujan_mul_unit

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

analytic-number-theorycircle-methodnumber-theoryramanujan-sums

Let $q\ge1$ and let $v$ be an integer that is invertible modulo $q$ . Then for every $n$ ,

c_q(vn)=c_q(n).

Ramanujan's sum depends on $n$ only through the subgroup structure: multiplying $n$ by a unit permutes the reduced residues in the defining sum. This invariance is what removes the auxiliary Bezout coefficients when the modulus of a Ramanujan sum is split by the Chinese remainder theorem.

Preamble

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

Formal statement

namespace Vino

theorem ramanujan_mul_unit (q : ℕ) [NeZero q] {v : ℤ} (hv : IsUnit ((v : ℤ) : ZMod q)) (n : ℤ) :
    ramanujan q (v * n) = ramanujan q n := 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