add_left

Mathlib.Data.Int.ModEq

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

English

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

Русский

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

LaTeX

$$(c \in \mathbb{Z})\;\; a \equiv b \pmod n \Rightarrow c + a \equiv c + b \pmod n$$

Lean4

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

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

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

Разделы

Аффилиация

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