add_comm_equiv

Mathlib.SetTheory.PGame.Algebra

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

English

For all x,y, x+y is equivalent to y+x.

Русский

Для любых x,y сумма x+y эквивалентна y+x.

LaTeX

$$$x + y \approx y + x$$$

Lean4

theorem add_comm_equiv {x y : PGame} : x + y ≈ y + x :=
  (x.add_comm y).equiv

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

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

Разделы

Аффилиация

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