Commit 2024-09-15 05:08 85bc2577

View on Github →

chore(SetTheory/Game/Nim): golf proof of Sprague-Grundy (#16349) We also add some useful auxiliary lemmas.

Estimated changes

Modified Mathlib/SetTheory/Game/Nim.lean

modified theorem SetTheory.PGame.equiv_nim_grundyValue

added theorem SetTheory.PGame.exists_grundyValue_left_of_lt

added theorem SetTheory.PGame.exists_grundyValue_right_of_lt

modified theorem SetTheory.PGame.grundyValue_eq_mex_right

added theorem SetTheory.PGame.grundyValue_ne_left

added theorem SetTheory.PGame.grundyValue_ne_right