mul_comm_equiv

Mathlib.SetTheory.Game.Basic

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

English

The equivalence relation identifies x*y with y*x; i.e., the two products are equivalent.

Русский

Эквивалентность идентифицирует x*y с y*x; то есть два произведения эквивалентны.

LaTeX

$$$$x \\cdot y \\equiv y \\cdot x.$$$$

Lean4

/-- `x * y` is equivalent to `y * x`. -/
theorem mul_comm_equiv (x y : PGame) : x * y ≈ y * x :=
  Quotient.exact <| quot_mul_comm _ _

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

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

Разделы

Аффилиация

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