cancel_right_div_gcd — Mathlib

English

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

Русский

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

LaTeX

$$$\\\\forall m,a,b,c \\\\in \\\\mathbb{N},\\\\ a c \\\\equiv b c \\\\pmod{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_right_div_gcd (hm : 0 < m) (h : a * c ≡ b * c [MOD m]) : a ≡ b [MOD m / gcd m c] :=
  by
  apply cancel_left_div_gcd hm
  simpa [mul_comm] using h

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