English
In the quotient of games by equivalence, the product is commutative: ⟦x*y⟧ = ⟦y*x⟧.
Русский
В частоте игр по эквивалентности произведение коммутативно: ⟦x*y⟧ = ⟦y*x⟧.
LaTeX
$$$$\\big[ x \\cdot y \\big] = \\big[ y \\cdot x \\big]$$$$
Lean4
/-- `x * y` and `y * x` have the same moves. -/
def mulCommRelabelling (x y : PGame.{u}) : x * y ≡r y * x :=
match x, y with
| ⟨xl, xr, xL, xR⟩, ⟨yl, yr, yL, yR⟩ => by
refine
⟨Equiv.sumCongr (Equiv.prodComm _ _) (Equiv.prodComm _ _),
(Equiv.sumComm _ _).trans (Equiv.sumCongr (Equiv.prodComm _ _) (Equiv.prodComm _ _)), ?_, ?_⟩ <;>
rintro (⟨i, j⟩ | ⟨i, j⟩) <;>
{ dsimp
exact
((addCommRelabelling _ _).trans <| (mulCommRelabelling _ _).addCongr (mulCommRelabelling _ _)).subCongr
(mulCommRelabelling _ _)
}
termination_by (x, y)
