cancel_right_of_coprime — Mathlib

English

If gcd(m,c) = 1 and a c ≡ b c (mod m), then a ≡ b (mod m).

Русский

Если gcd(m,c) = 1 и a c ≡ b c (mod m), то a ≡ b (mod m).

LaTeX

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

Lean4

/-- A common factor that's coprime with the modulus can be cancelled from a `ModEq` -/
theorem cancel_right_of_coprime (hmc : gcd m c = 1) (h : a * c ≡ b * c [MOD m]) : a ≡ b [MOD m] :=
  cancel_left_of_coprime hmc <| by simpa [mul_comm] using h

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