quot_one_mul

Mathlib.SetTheory.Game.Basic

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

English

The quotient of 1*x equals the quotient of x.

Русский

Часть 1*x эквивалентно части x.

LaTeX

$$$[ 1 \cdot x ] = [ x ]$$$

Lean4

@[simp]
theorem quot_one_mul (x : PGame) : (⟦1 * x⟧ : Game) = ⟦x⟧ :=
  game_eq x.one_mul.equiv

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

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

Разделы

Аффилиация

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