Representative of a residue class

Proved

Vino.intCast_sub_val_dvd

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

algebranumber-theory

If an integer $m$ reduces to $x\in\mathbb Z/q\mathbb Z$ , then $m$ differs from the canonical representative $\tilde x\in\{0,\dots,q-1\}$ by a multiple of $q$ :

q\mid m-\tilde x .

This is the bridge between arithmetic in $\mathbb Z/q\mathbb Z$ and the integer numerators that appear inside the additive character $e(\cdot/q)$ .

Preamble

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

Formal statement

namespace Vino

theorem intCast_sub_val_dvd {q : ℕ} [NeZero q] (m : ℤ) (x : ZMod q) (h : (m : ZMod q) = x) :
    (q : ℤ) ∣ (m - (x.val : ℤ)) := 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