add_left_cancel — Mathlib

English

If a ≡ b (mod n) and a + c ≡ b + d (mod n), then c ≡ d (mod n).

Русский

Если a ≡ b (mod n) и a + c ≡ b + d (mod n), то c ≡ d (mod n).

LaTeX

$$$a \equiv b \pmod n \land a + c \equiv b + d \pmod n \Rightarrow c \equiv d \pmod n$$$

Lean4

protected theorem add_left_cancel (h₁ : a ≡ b [ZMOD n]) (h₂ : a + c ≡ b + d [ZMOD n]) : c ≡ d [ZMOD n] :=
  have : d - c = b + d - (a + c) - (b - a) := by cutsat
  modEq_iff_dvd.2 <| by
    rw [this]
    exact Int.dvd_sub h₂.dvd h₁.dvd

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