Congruence_by_Divisor_of_Modulus
Provedmodular-arithmeticproofwiki
Let a be congruent to b modulo z. If m divides z, then a is congruent to b modulo m.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Congruence_by_Divisor_of_Modulus (a b z m : ℤ) (hz : m ∣ z) (h : z ∣ (a - b)) : m ∣ (a - b) := by sorry
Source