mul_one

Mathlib.SetTheory.Game.Basic

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

English

x * 1 is equivalent to x.

Русский

x умножение на единицу эквивалентно x.

LaTeX

$$x \cdot 1 \approx x$$

Lean4

/-- `x * 1` has the same moves as `x`. -/
protected theorem mul_one (x : PGame) : x * 1 ≡ x :=
  (x.mul_comm _).trans x.one_mul

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

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

Разделы

Аффилиация

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