Commit 2023-06-29 14:30 4206dd5c

View on Github →

feat: port SetTheory.Game.Nim (#5550)

Estimated changes

Modified Mathlib.lean

Created Mathlib/SetTheory/Game/Nim.lean

added theorem PGame.default_nim_one_leftMoves_eq

added theorem PGame.default_nim_one_rightMoves_eq

added theorem PGame.equiv_nim_grundyValue

added theorem PGame.grundyValue_add

added theorem PGame.grundyValue_eq_iff_equiv

added theorem PGame.grundyValue_eq_iff_equiv_nim

added theorem PGame.grundyValue_eq_mex_left

added theorem PGame.grundyValue_eq_mex_right

added theorem PGame.grundyValue_iff_equiv_zero

added theorem PGame.grundyValue_neg

added theorem PGame.grundyValue_nim_add_nim

added theorem PGame.grundyValue_star

added theorem PGame.grundyValue_zero

added def PGame.leftMovesNimRecOn

added theorem PGame.leftMoves_nim

added theorem PGame.moveLeft_nim'

added theorem PGame.moveLeft_nim

added theorem PGame.moveLeft_nim_hEq

added theorem PGame.moveRight_nim'

added theorem PGame.moveRight_nim

added theorem PGame.moveRight_nim_hEq

added theorem PGame.neg_nim

added def PGame.nimOneRelabelling

added def PGame.nimZeroRelabelling

added theorem PGame.nim_add_equiv_zero_iff

added theorem PGame.nim_add_fuzzy_zero_iff

added theorem PGame.nim_add_nim_equiv

added theorem PGame.nim_birthday

added theorem PGame.nim_def

added theorem PGame.nim_equiv_iff_eq

added theorem PGame.nim_fuzzy_zero_of_ne_zero

added theorem PGame.nim_grundyValue

added theorem PGame.nim_one_equiv

added theorem PGame.nim_one_moveLeft

added theorem PGame.nim_one_moveRight

added theorem PGame.nim_zero_equiv

added def PGame.rightMovesNimRecOn

added theorem PGame.rightMoves_nim

added theorem PGame.toLeftMovesNim_one_symm

added theorem PGame.toLeftMovesNim_symm_lt

added theorem PGame.toRightMovesNim_one_symm

added theorem PGame.toRightMovesNim_symm_lt