add_right_cancel'

Mathlib.Data.Int.ModEq

URI: https://scilib.ai/kg/mathlib#Int.ModEq.add_right_cancel'

English

For any c, if a + c ≡ b + c (mod n), then a ≡ b (mod n).

Русский

Для любого c, если a + c ≡ b + c (mod n), то a ≡ b (mod n).

LaTeX

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

Lean4

protected theorem add_right_cancel' (c : ℤ) (h : a + c ≡ b + c [ZMOD n]) : a ≡ b [ZMOD n] :=
  ModEq.rfl.add_right_cancel h

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru