neg_mk_mul_moveLeft_inl — Mathlib

English

For i ∈ xl and j ∈ yl, the left move of the negated product -(x*y) corresponding to the left-inl index equals the negation of the corresponding left-hand decomposition.

Русский

Для i ∈ xl и j ∈ yl левый ход отрицательного произведения -(x*y), соответствующий inl, равен отрицанию соответствующего разложения слева.

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 neg_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 * yR j - xL i * yR j) :=
  rfl

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