English
Let m > 0 and a c ≡ b c (mod m). Then a ≡ b (mod m / gcd(m,c)).
Русский
Пусть m > 0 и a c ≡ b c (mod m). Тогда a ≡ b (mod m / gcd(m,c)).
LaTeX
$$$0 < m \\land a c \\equiv b c [ZMOD m] \\Rightarrow a \\equiv b [ZMOD m / \\gcd(m,c)].$$$
Lean4
/-- To cancel a common factor `c` from a `ModEq` we must divide the modulus `m` by `gcd m c`. -/
theorem cancel_right_div_gcd (hm : 0 < m) (h : a * c ≡ b * c [ZMOD m]) : a ≡ b [ZMOD m / gcd m c] :=
by
letI d := gcd m c
rw [modEq_iff_dvd] at h ⊢
refine Int.dvd_of_dvd_mul_right_of_gcd_one (?_ : m / d ∣ c / d * (b - a)) ?_
· rw [mul_comm, ← Int.mul_ediv_assoc (b - a) (gcd_dvd_right ..), Int.sub_mul]
exact Int.ediv_dvd_ediv (gcd_dvd_left ..) h
· rw [gcd_div (gcd_dvd_left ..) (gcd_dvd_right ..), natAbs_natCast, Nat.div_self (gcd_pos_of_ne_zero_left c hm.ne')]
