Prove2Me

cq(n)=φ(q)c_q(n)=\varphi(q) when q∣nq\mid n

Proved
Vino.ramanujan_eq_totient_of_dvd

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

analytic-number-theorycircle-methodnumber-theoryramanujan-sums

If qq divides nn then every term of Ramanujan's sum is 11, so

cq(n)=φ(q)whenever q∣n.c_q(n)=\varphi(q)\qquad\text{whenever }q\mid n.

This generalises cq(0)=φ(q)c_q(0)=\varphi(q) and identifies the extreme case of the bound ∣cq(n)∣≤φ(q)|c_q(n)|\le\varphi(q): the sum is maximal exactly on the residue class where the local condition is vacuous.

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_eq_totient_of_dvd {q : ℕ} (hq : 0 < q) {n : ℤ} (h : (q : ℤ) ∣ n) :
    ramanujan q n = (Nat.totient q : ℂ) := 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