sub_eq_add

Mathlib.Data.ZMod.Basic

URI: https://scilib.ai/kg/mathlib#ZModModule.sub_eq_add

English

In characteristic 2, subtraction coincides with addition: x − y = x + y.

Русский

В характеристике 2 вычитание совпадает с сложением: x − y = x + y.

LaTeX

$$$x - y = x + y$$$

Lean4

theorem sub_eq_add (x y : G) : x - y = x + y := by simp [neg_eq_self, sub_eq_add_neg]

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

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

Разделы

Аффилиация

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