English
There is a natural equivalence between (x.LeftMoves × y.LeftMoves) ⊕ (x.RightMoves × y.RightMoves) and (x*y).LeftMoves, identifying the two representations of the left moves of the product.
Русский
Существует естественная эквивалентность между суммой левых ходов и правых ходов и левыми ходами произведения, идентифицирующая два описания левых ходов произведения.
LaTeX
$$$ (x.LeftMoves \times y.LeftMoves) \oplus (x.RightMoves \times y.RightMoves) \simeq (x * y).LeftMoves $$$
Lean4
/-- Turns two left or right moves for `x` and `y` into a left move for `x * y` and vice versa.
Even though these types are the same (not definitionally so), this is the preferred way to convert
between them. -/
def toLeftMovesMul {x y : PGame} : (x.LeftMoves × y.LeftMoves) ⊕ (x.RightMoves × y.RightMoves) ≃ (x * y).LeftMoves :=
Equiv.cast (leftMoves_mul x y).symm
