Counting reduced residues gives Euler's totient

Proved

Vino.card_coprime_filter

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

analytic-number-theorycircle-methodnumber-theoryramanujan-sums

The number of $a$ with $0\le a<q$ and $(a,q)=1$ is Euler's totient:

\#\{a<q:\gcd(a,q)=1\}=\varphi(q).

Mathlib defines $\varphi$ by the same count but with the arguments of Nat.Coprime in the opposite order; this lemma records that the two agree, and it is what turns counting bounds on Ramanujan sums into bounds in terms of $\varphi$ .

Preamble

import Definitions.Def_Vino_ramanujan
import Mathlib.Data.Nat.Totient
open Finset

Formal statement

namespace Vino

theorem card_coprime_filter (q : ℕ) :
    (((Finset.range q).filter (fun a => Nat.Coprime a q)).card) = Nat.totient q := 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