quot_neg_mul_neg

Mathlib.SetTheory.Game.Basic

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

English

The quotient of (-x) * (-y) equals the quotient of x*y.

Русский

Часть (-x) * (-y) эквивалентна части x*y.

LaTeX

$$$[ -x \cdot -y ] = [ x \cdot y ]$$$

Lean4

theorem quot_neg_mul_neg (x y : PGame) : ⟦-x * -y⟧ = (⟦x * y⟧ : Game) := by simp

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

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

Разделы

Аффилиация

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