sub_zero_eq_add_zero

Mathlib.SetTheory.PGame.Algebra

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

English

For any PGame x, subtracting zero yields the same game as adding zero: x - 0 = x + 0.

Русский

Для любого PGame x вычитание нуля даёт тот же результат, что и сложение с нулём: x − 0 = x + 0.

LaTeX

$$$x - 0 = x + 0$$$

Lean4

@[simp]
theorem sub_zero_eq_add_zero (x : PGame) : x - 0 = x + 0 :=
  show x + -0 = x + 0 by rw [neg_zero]

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

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

Разделы

Аффилиация

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