English
The product of two games is commutative up to equivalence: x*y is equivalent to y*x.
Русский
Произведение двух игр коммутативно до эквивалентности: x*y эквивалентно y*x.
LaTeX
$$$$x \\cdot y \\equiv y \\cdot x.$$$$
Lean4
/-- `x * y` and `y * x` have the same moves. -/
protected theorem mul_comm (x y : PGame) : x * y ≡ y * x :=
match x, y with
| ⟨xl, xr, xL, xR⟩, ⟨yl, yr, yL, yR⟩ => by
refine
Identical.of_equiv ((Equiv.prodComm _ _).sumCongr (Equiv.prodComm _ _))
((Equiv.sumComm _ _).trans ((Equiv.prodComm _ _).sumCongr (Equiv.prodComm _ _))) ?_ ?_ <;>
·
rintro (⟨_, _⟩ | ⟨_, _⟩) <;>
exact
((((PGame.mul_comm _ (mk _ _ _ _)).add (PGame.mul_comm (mk _ _ _ _) _)).trans (PGame.add_comm _ _)).sub
(PGame.mul_comm _ _))
termination_by (x, y)
