Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-30 04:53 a18f142d

View on Github →

feat(set_theory/game): computation of grundy_value (nim n + nim m) (#3977)

Estimated changes

Modified src/data/nat/bitwise.lean

added theorem nat.lxor_trichotomy

Modified src/set_theory/game/nim.lean

added theorem pgame.equiv_iff_grundy_value_eq

modified theorem pgame.equiv_nim_iff_grundy_value_eq

added theorem pgame.equiv_zero_iff_grundy_value

added theorem pgame.grundy_value_add

added theorem pgame.grundy_value_nim_add_nim

added theorem pgame.grundy_value_zero

added theorem pgame.nim.exists_move_left_eq

added theorem pgame.nim.exists_ordinal_move_left_eq

added theorem pgame.nim_add_nim_equiv

Modified src/set_theory/pgame.lean

added theorem pgame.equiv_congr_left

added theorem pgame.equiv_congr_right