Reduced residues modulo a prime

Proved

Vino.filter_coprime_prime

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

analytic-number-theorycircle-methodnumber-theoryramanujan-sums

If $p$ is prime, the reduced residues below $p$ are exactly the nonzero residues:

\{a<p:\gcd(a,p)=1\}=\{1,2,\dots,p-1\}.

This is what lets a complete exponential sum modulo $p$ be converted into a Ramanujan sum by removing a single term.

Preamble

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

Formal statement

namespace Vino

theorem filter_coprime_prime {p : ℕ} (hp : p.Prime) :
    (Finset.range p).filter (fun a => Nat.Coprime a p) = (Finset.range p).erase 0 := 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