cancel_right_div_gcd' — Mathlib

English

If a c ≡ b d (mod m) with c ≡ d (mod m), then a c ≡ b c (mod m) implies a ≡ b (mod m / gcd c).

Русский

Если a c ≡ b d (mod m) и c ≡ d (mod m), то a c ≡ b c (mod m) дает a ≡ b (mod m / gcd c).

LaTeX

$$$\\\\forall m,a,b,c \\\\in \\\\mathbb{N},\\\\ a c \\\\equiv b d \\\\pmod{m} \\\\land \\\\ c \\\\equiv d \\\\pmod{m} \\\\Rightarrow a c \\\\equiv b c \\\\pmod{\\\\frac{m}{\\\\gcd(m,c)}}$$$

Lean4

theorem cancel_right_div_gcd' (hm : 0 < m) (hcd : c ≡ d [MOD m]) (h : a * c ≡ b * d [MOD m]) :
    a ≡ b [MOD m / gcd m c] :=
  (h.trans <| hcd.symm.mul_left b).cancel_right_div_gcd hm

Похожие утверждения