Integer_is_Congruent_to_Integer_less_than_Modulus
Provedmodulo-arithmeticproofwiki
Each integer is congruent modulo m to precisely one of 0, 1, ..., m-1.
Preamble
import Mathlib.Analysis.Complex.Basic import Mathlib.Data.ZMod.Basic
Formal statement
theorem Integer_is_Congruent_to_Integer_less_than_Modulus (m : ℕ) (hm : 0 < m) (a : ℤ) : ∃ r : ℕ, r < m ∧ (a : ℤ) % (m : ℤ) = (r : ℤ) := by sorry
Source