neg

Mathlib.Data.Int.ModEq

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

English

Let a ≡ b (mod n). Then −a ≡ −b (mod n).

Русский

Пусть a ≡ b (mod n). Тогда −a ≡ −b (mod n).

LaTeX

$$$a \equiv b \pmod n \Rightarrow -a \equiv -b \pmod n$$$

Lean4

@[gcongr]
protected theorem neg (h : a ≡ b [ZMOD n]) : -a ≡ -b [ZMOD n] :=
  h.add_left_cancel (by simp_rw [← sub_eq_add_neg, sub_self]; rfl)

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

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

Разделы

Аффилиация

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