Ramanujan sums are even in $n$

Proved

Vino.ramanujan_neg_arg

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

analytic-number-theorycircle-methodnumber-theoryramanujan-sums

For every modulus $q$ and every integer $n$ ,

c_q(-n)=c_q(n).

Combined with $c_q(-n)=\overline{c_q(n)}$ this is what makes Ramanujan sums real. Directly, it reflects the fact that the local conditions counted by the singular series are insensitive to the sign of the target $n$ .

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 ramanujan_neg_arg (q : ℕ) (n : ℤ) : ramanujan q (-n) = ramanujan q 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

Ramanujan sums are even in nnn

Ramanujan sums are even in $n$