neg_mk_mul_moveLeft_inr — Mathlib

English

For i ∈ xr and j ∈ yr, the left move of the negated product -(x*y) corresponding to the inr index equals the negation of the corresponding decomposition with right-hand parts.

Русский

Для i ∈ xr и j ∈ yr левый ход отрицательного произведения -(x*y) соответствующий inr равен отрицанию соответствующего разложения с правыми компонентами.

LaTeX

$$$$-(x*y).moveLeft(\\mathrm{toLeftMovesMul}(\\mathrm{Sum.inr}(i,j))) = -(x^{R}(i) \\cdot y + x \\cdot y^{R}(j) - x^{R}(i) \\cdot y^{R}(j))$$$$

Lean4

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

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