Common_Factor_Cancelling_in_Congruence
Provedmodular-arithmeticnumber-theoryproofwiki
If ax is congruent to by (mod m) and a is congruent to b (mod m), then x is congruent to y (mod m/gcd(a,m)).
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Common_Factor_Cancelling_in_Congruence (a b x y m : ℤ) (hab : a ≡ b [ZMOD m]) (hax : a * x ≡ b * y [ZMOD m]) (hm : m ≠ 0) : x ≡ y [ZMOD (m / Int.gcd a m)] := by sorry
Source