neg_mul

Mathlib.SetTheory.Game.Basic

URI: https://scilib.ai/kg/mathlib#SetTheory.PGame.neg_mul

← MathLib Explorer

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. -/
theorem neg_mul (x y : PGame) : -x * y ≡ -(x * y) :=
  ((PGame.mul_comm _ _).trans (of_eq (mul_neg _ _))).trans (PGame.mul_comm _ _).neg

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru