cancel_left_div_gcd' — Mathlib

English

If nonzero m and m.gcd(c) divides the product-modEq, then a ≡ b modulo m.gcd(c).

Русский

Если m > 0 и gcd(m,c) делит мод-эквивалентную разницу, тогда a ≡ b по модулю 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

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

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