mk_mul_moveRight_inr — Mathlib

English

For i ∈ x.RightMoves and j ∈ y.RightMoves, the right move of the product x*y with the inr index equals xR(i)·y + x·yR(j) − xR(i)·yR(j).

Русский

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

LaTeX

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

Lean4

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

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