add_add_add_cancel

Mathlib.Data.ZMod.Basic

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

English

For all x,y,z, (x+y)+(y+z) = x+z in characteristic 2.

Русский

Для всех x,y,z выполняется (x+y)+(y+z) = x+z при характеристике 2.

LaTeX

$$$ (x + y) + (y + z) = x + z $$$

Lean4

theorem add_add_add_cancel (x y z : G) : (x + y) + (y + z) = x + z := by
  simpa [sub_eq_add] using sub_add_sub_cancel x y z

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

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

Разделы

Аффилиация

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