mul_neg — Mathlib

English

For all x,y, x * (-y) = -(x*y).

Русский

Для любых x,y выполнено x * (−y) = −(x*y).

LaTeX

$$$x \cdot (-y) = -(x \cdot y)$$$

Lean4

/-- `x * -y` and `-(x * y)` have the same moves. -/
@[simp]
theorem mul_neg (x y : PGame) : x * -y = -(x * y) :=
  match x, y with
  | mk xl xr xL xR, mk yl yr yL yR =>
    by
    refine ext rfl rfl ?_ ?_ <;> rintro (⟨i, j⟩ | ⟨i, j⟩) _ ⟨rfl⟩
    all_goals
      dsimp
      rw [PGame.neg_sub', PGame.neg_add]
      congr
      exacts [mul_neg _ (mk ..), mul_neg .., mul_neg ..]
termination_by (x, y)

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