quot_zero_mul

Mathlib.SetTheory.Game.Basic

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

English

For every PGame x, the product of 0 and x is the zero game.

Русский

Для любого PGame x произведение 0 на x эквивалентно нулевой игре.

LaTeX

$$$0 \cdot x = 0$$$

Lean4

@[simp]
theorem quot_zero_mul (x : PGame) : (⟦0 * x⟧ : Game) = 0 :=
  game_eq x.zero_mul_equiv

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

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

Разделы

Аффилиация

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