modEq_add_fac — Mathlib

English

For Ne(c,0), c*a ≡ c*b [ZMOD c*m] ↔ m ≡ a ≡ b [ZMOD m].

Русский

Для c ≠ 0 верно: c*a ≡ c*b [ZMOD c*m] эквивалентно a ≡ b [ZMOD m].

LaTeX

$$$\\forall {m a b : \\mathbb{Z}}, \\; \\mathrm{Ne}(c,0) \\Rightarrow (c a \\equiv c b [ZMOD c m]) \\iff (a \\equiv b [ZMOD m]).$$$

Lean4

theorem modEq_add_fac {a b n : ℤ} (c : ℤ) (ha : a ≡ b [ZMOD n]) : a + n * c ≡ b [ZMOD n] :=
  calc
    a + n * c ≡ b + n * c [ZMOD n] := ha.add_right _
    _ ≡ b + 0 [ZMOD n] := ((dvd_mul_right _ _).modEq_zero_int.add_left _)
    _ ≡ b [ZMOD n] := by rw [add_zero]

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