Ramanujan sums are multiplicative in the modulus

Proved

Vino.ramanujan_mul_coprime

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

analytic-number-theorycircle-methodnumber-theoryramanujan-sums

If $(q_1,q_2)=1$ then for every integer $n$ ,

c_{q_1q_2}(n)=c_{q_1}(n)\,c_{q_2}(n).

Multiplicativity in the modulus is the structural fact that makes the singular series an Euler product. Together with the multiplicativity of $\mu$ and of $\varphi$ it shows that $q\mapsto\mu(q)c_q(n)/\varphi(q)^3$ is multiplicative, so that $\sum_{q\mid Q}\mu(q)c_q(n)/\varphi(q)^3$ factors over the primes dividing $Q$ .

Preamble

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

Formal statement

namespace Vino

theorem ramanujan_mul_coprime {q₁ q₂ : ℕ} (h : Nat.Coprime q₁ q₂) (n : ℤ) :
    ramanujan (q₁ * q₂) n = ramanujan q₁ 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