neg_add_rev

Mathlib.SetTheory.PGame.Algebra

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

← MathLib Explorer

English

Negation of a sum reverses the order: −(x+y) ≡ −y + −x.

Русский

Отрицание суммы меняет порядок действий: −(x+y) ≡ −y + −x.

LaTeX

$$$ -(x+y) \equiv -y + -x $$$

Lean4

/-- `-(x + y)` has exactly the same moves as `-y + -x`. -/
protected theorem neg_add_rev (x y : PGame) : -(x + y) ≡ -y + -x :=
  Identical.trans (of_eq (x.neg_add y)) (PGame.add_comm _ _)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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