cancel_left_div_gcd — Mathlib

English

Let m > 0 and c a ≡ c b (mod m). Then a ≡ b (mod m / gcd(m,c)).

Русский

Пусть m > 0 и c·a ≡ c·b (mod m). Тогда a ≡ b (mod m / gcd(m,c)).

LaTeX

$$$0 < m \\land c a \\equiv c b [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_left_div_gcd (hm : 0 < m) (h : c * a ≡ c * b [ZMOD m]) : a ≡ b [ZMOD m / gcd m c] :=
  cancel_right_div_gcd hm <| by simpa [mul_comm] using h

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