add_self

Mathlib.SetTheory.Game.Impartial

URI: https://scilib.ai/kg/mathlib#SetTheory.PGame.Impartial.add_self

English

For an impartial G, the sum G + G is equivalent to 0: G + G ≈ 0.

Русский

Для непредвзятой G сумма G + G эквивалентна 0.

LaTeX

$$$G + G \approx 0$$$

Lean4

theorem add_self : G + G ≈ 0 :=
  Equiv.trans (add_congr_left (neg_equiv_self G)) (neg_add_cancel_equiv G)

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

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

Разделы

Аффилиация

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