nimOneRelabelling — Mathlib

English

The game Nim(1) is equivalent to the star game; i.e., Nim(1) ≈ star.

Русский

Игра Nim(1) эквивалентна игре звезда; то есть Nim(1) ≈ star.

LaTeX

$$$ \mathrm{nim}(1) \approx \mathrm{star}. $$$

Lean4

/-- `nim 1` has exactly the same moves as `star`. -/
def nimOneRelabelling : nim 1 ≡r star := by
  rw [nim]
  refine ⟨?_, ?_, fun i => ?_, fun j => ?_⟩
  any_goals dsimp; apply Equiv.ofUnique
  all_goals simpa [enumIsoToType] using nimZeroRelabelling

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