English
For i ∈ x.LeftMoves and j ∈ y.LeftMoves, the left move of the product x*y with the left-inl index equals x moveLeft i times y, plus x times y moveLeft j, minus x moveLeft i times y moveLeft j.
Русский
Для i ∈ x.LeftMoves и j ∈ y.LeftMoves левый ход произведения x*y, соответствующий левому компоненту, равен x.moveLeft(i)·y + x·y.moveLeft(j) − x.moveLeft(i)·y.moveLeft(j).
LaTeX
$$$$(x * y).moveLeft(\\mathrm{toLeftMovesMul}(\\mathrm{Sum.inl}(i,j))) = x.moveLeft(i) \\cdot y + x \\cdot y.moveLeft(j) - x.moveLeft(i) \\cdot y.moveLeft(j)$$$$
Lean4
@[simp]
theorem mul_moveLeft_inl {x y : PGame} {i j} :
(x * y).moveLeft (toLeftMovesMul (Sum.inl (i, j))) =
x.moveLeft i * y + x * y.moveLeft j - x.moveLeft i * y.moveLeft j :=
by
cases x
cases y
rfl
