Commit 2024-10-13 23:54 9a1b545e

View on Github →

feat(SetTheory/Game/Nim): make grundyValue a nimber (#17645) We redefine the grundy value of an impartial game as a nimber. That way, we can prove a more general form of grundyValue_add.

Estimated changes

Modified Mathlib/SetTheory/Game/Nim.lean

modified theorem SetTheory.PGame.equiv_nim_grundyValue

modified theorem SetTheory.PGame.exists_grundyValue_moveLeft_of_lt

modified theorem SetTheory.PGame.exists_grundyValue_moveRight_of_lt

modified theorem SetTheory.PGame.grundyValue_add

modified theorem SetTheory.PGame.grundyValue_eq_iff_equiv_nim

modified theorem SetTheory.PGame.grundyValue_iff_equiv_zero

modified theorem SetTheory.PGame.grundyValue_le_of_forall_moveLeft

modified theorem SetTheory.PGame.grundyValue_le_of_forall_moveRight

modified theorem SetTheory.PGame.grundyValue_nim_add_nim

modified theorem SetTheory.PGame.le_grundyValue_of_Iio_subset_moveLeft

modified theorem SetTheory.PGame.le_grundyValue_of_Iio_subset_moveRight

modified theorem SetTheory.PGame.nim_add_nim_equiv

modified theorem SetTheory.PGame.nim_grundyValue

Modified Mathlib/SetTheory/Ordinal/Nimber.lean

added theorem Nimber.lt_add_cases