mk_mul_moveRight_inl — Mathlib

English

For i ∈ x.LeftMoves and j ∈ y.LeftMoves, the right move of the product x*y with the left-inl index equals xL(i)·y + x·yR(j) − xL(i)·yR(j).

Русский

Для i ∈ x.LeftMoves и j ∈ y.LeftMoves правый ход произведения x*y, соответствующий inl, равен xL(i)·y + x·yR(j) − xL(i)·yR(j).

LaTeX

$$$$(mk xl xr xL xR * mk yl yr yL yR).moveRight(\\mathrm{toRightMovesMul}(\\mathrm{Sum.inl}(i,j))) = xL(i) \\cdot mk yl yr yL yR + mk xl xr xL xR \\cdot yR(j) - xL(i) \\cdot yR(j)$$$$

Lean4

@[simp]
theorem mk_mul_moveRight_inl {xl xr yl yr} {xL xR yL yR} {i j} :
    (mk xl xr xL xR * mk yl yr yL yR).moveRight (Sum.inl (i, j)) =
      xL i * mk yl yr yL yR + mk xl xr xL xR * yR j - xL i * yR j :=
  rfl

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