Ramanujan sums are integers

Proved

Vino.ramanujan_isInt

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

analytic-number-theorycircle-methodnumber-theoryramanujan-sums

Although it is defined as a sum of $\varphi(q)$ complex roots of unity, Ramanujan's sum is an integer: for all $q$ and $n$ there is $m\in\mathbb Z$ with

c_q(n)=m.

Integrality is immediate from Kluyver's formula, whose terms are $d\,\mu(q/d)$ with $d\mid\gcd(q,n)$ . It is the reason $c_q(n)$ can be treated as an arithmetic rather than an analytic object, and in particular why the singular series has rational partial sums.

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_isInt (q : ℕ) (n : ℤ) : ∃ m : ℤ, ramanujan q n = (m : ℂ) := 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