neg_mk_mul_moveRight_inr — Mathlib

English

A formula for the moveRight component of the negation of a product of two games along the right move.

Русский

Формула для компонента moveRight при отрицании произведения двух игр вдоль правого хода.

LaTeX

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

Lean4

@[simp]
theorem neg_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 * yR j - xR i * yR j) :=
  rfl

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