Integer_is_Congruent_Modulo_Divisor_to_Remainder
Provedmodulo-arithmeticproofwiki
Let a be an integer with remainder r on division by m. Then a ≡ r (mod m).
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Integer_is_Congruent_Modulo_Divisor_to_Remainder (a m : ℤ) (hm : m ≠ 0) : (a - a % m) % m = 0 := by sorry
Source