add_assoc_equiv

Mathlib.SetTheory.PGame.Algebra

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

English

For all x,y,z, x+y+z ≈ x+(y+z).

Русский

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

LaTeX

$$$x + y + z \approx x + (y + z)$$$

Lean4

theorem add_assoc_equiv {x y z : PGame} : x + y + z ≈ x + (y + z) :=
  (x.add_assoc y z).equiv

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

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

Разделы

Аффилиация

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