cancel_left_of_coprime — Mathlib

English

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

Русский

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

LaTeX

$$$\\\\forall m\\\\, a\\\\, b\\\\, c \\\\in \\\\mathbb{N},\\\\ gcd(m,c) = 1 \\\\land \\\\ c a \\\\equiv c b \\\\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_left_of_coprime (hmc : gcd m c = 1) (h : c * a ≡ c * b [MOD m]) : a ≡ b [MOD m] :=
  by
  rcases m.eq_zero_or_pos with (rfl | hm)
  · simp only [gcd_zero_left] at hmc
    simp only [hmc, one_mul, modEq_zero_iff] at h
    subst h
    rfl
  simpa [hmc] using h.cancel_left_div_gcd hm

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