mk_mul_moveLeft_inl — Mathlib

English

For x = mk xl xr xL xR and y = mk yl yr yL yR and i ∈ xl, j ∈ yl, the left move of the product x*y corresponding to the left component (inl side) equals xL(i)·y + x·yL(j) − xL(i)·yL(j).

Русский

Пусть x = mk xl xr xL xR и y = mk yl yr yL yR, и i ∈ xl, j ∈ yl. Тогда левый ход произведения x*y, соответствующий компоненту слева (inl), равен xL(i)·y + x·yL(j) − xL(i)·yL(j).

LaTeX

$$$$(x*y).moveLeft(\\mathrm{inl}(i,j)) = x^{L}(i) \\cdot y + x \\cdot y^{L}(j) - x^{L}(i) \\cdot y^{L}(j)$$$$

Lean4

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

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