English
Let m > 0 and gcd-related factor c. If c a ≡ c b (mod m), then a ≡ b (mod m / gcd(m,c)).
Русский
Пусть m > 0 и имеется фактор c так, что gcd(m,c) учитывается. Если c a ≡ c b (mod m), то a ≡ b (mod m / gcd(m,c)).
LaTeX
$$$\\\\forall m,a,b,c \\\\in \\\\mathbb{N},\\\\ m > 0 \\\\land \\\\mathrm{ModEq}(c a, c b; m) \\\\Rightarrow a \\\\equiv b \\\\pmod{\\\\frac{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_left_div_gcd (hm : 0 < m) (h : c * a ≡ c * b [MOD m]) : a ≡ b [MOD m / gcd m c] :=
by
let d := gcd m c
have hmd := gcd_dvd_left m c
have hcd := gcd_dvd_right m c
rw [modEq_iff_dvd]
refine @Int.dvd_of_dvd_mul_right_of_gcd_one (m / d) (c / d) (b - a) ?_ ?_
· show (m / d : ℤ) ∣ c / d * (b - a)
rw [mul_comm, ← Int.mul_ediv_assoc (b - a) (Int.natCast_dvd_natCast.mpr hcd), mul_comm]
apply Int.ediv_dvd_ediv (Int.natCast_dvd_natCast.mpr hmd)
rw [Int.mul_sub]
exact modEq_iff_dvd.mp h
· show Int.gcd (m / d) (c / d) = 1
simp only [d, ← Int.natCast_div, Int.gcd_natCast_natCast (m / d) (c / d), gcd_div hmd hcd,
Nat.div_self (gcd_pos_of_pos_left c hm)]
