neg_eq_self_mod_two

Mathlib.Data.ZMod.Basic

URI: https://scilib.ai/kg/mathlib#ZMod.neg_eq_self_mod_two

English

In ZMod 2, every element is its own negation.

Русский

В ZMod 2 каждый элемент есть собственное отрицание.

LaTeX

$$$-a = a$ for all $a \in \mathbb{Z}/2\mathbb{Z}$$$

Lean4

@[simp]
theorem neg_eq_self_mod_two (a : ZMod 2) : -a = a := by fin_cases a <;> apply Fin.ext <;> simp; rfl

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

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

Разделы

Аффилиация

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