grundyValue_star

Mathlib.SetTheory.Game.Nim

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

English

Grundy value of the star game is 1: grundyValue(star) = 1.

Русский

Грандивая величина звезды равна 1: grundyValue(star) = 1.

LaTeX

$$$ \operatorname{grundyValue}(\mathrm{star}) = 1. $$$

Lean4

@[simp]
theorem grundyValue_star : grundyValue star = 1 :=
  grundyValue_eq_iff_equiv_nim.2 (Equiv.symm nim_one_equiv)

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

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

Разделы

Аффилиация

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