Residues of a given gcd form a Ramanujan sum

Proved

Vino.fiber_gcd_eq_ramanujan

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

analytic-number-theorycircle-methodnumber-theoryramanujan-sums

Let $q\ge1$ and let $d$ be a divisor of $q$ . The residues $k<q$ with $\gcd(q,k)=d$ contribute to the complete exponential sum exactly a Ramanujan sum of the smaller modulus $q/d$ :

\sum_{\substack{k<q\\ \gcd(q,k)=d}}e\!\left(\frac{kn}{q}\right)\;=\;c_{q/d}(n).

Writing $k=d\,a$ identifies the fibre with the reduced residues modulo $q/d$ , and the phase $kn/q$ becomes $an/(q/d)$ . This is the fibrewise step that turns the complete sum $\sum_{k<q}e(kn/q)$ into a sum of Ramanujan sums over the divisors of $q$ , and hence — by Möbius inversion — gives Kluyver's closed formula.

Preamble

import Definitions.Def_Vino_ramanujan
import Mathlib.NumberTheory.Divisors
import Mathlib.NumberTheory.ArithmeticFunction.Moebius
import Mathlib.Data.Nat.Totient
open Finset

Formal statement

namespace Vino

theorem fiber_gcd_eq_ramanujan {q : ℕ} (hq : 0 < q) (n : ℤ) {d : ℕ} (hd : d ∈ q.divisors) :
    ∑ k ∈ (Finset.range q).filter (fun k => Nat.gcd q k = d),
        CircleMethod.e ((k : ℝ) * (n : ℝ) / (q : ℝ))
      = ramanujan (q / d) n := by sorry

end Vino

Source

G. H. Hardy and E. M. Wright, An Introduction to the Theory of Numbers, 6th ed., Oxford University Press, 2008, Section 16.6, Theorem 271 (Ramanujan's sum c_q(n) = sum over d | gcd(q,n) of d * mu(q/d)); J. C. Kluyver, Some formulae concerning the integers less than n and prime to n, Proc. Royal Netherlands Academy 9 (1906), 408-414.

View graph