moveRight_nim — Mathlib

English

For any i in (nim o).RightMoves, (nim o).moveRight i equals nim (toRightMovesNim i).val.

Русский

Для любого i из (nim o).RightMoves, (nim o).moveRight i равно nim (toRightMovesNim i).val.

LaTeX

$$$ \forall i\in (nim\ o).RightMoves,\; (nim\ o).moveRight\,i = nim\bigl((toRightMovesNim^{-1} i).val\bigr) $$$

Lean4

@[simp]
theorem moveRight_nim {o : Ordinal} (i) : (nim o).moveRight i = nim (toRightMovesNim.symm i).val :=
  (congr_heq (moveRight_nim_heq o).symm (cast_heq _ i)).symm

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