Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-04 20:04 28568bdb

View on Github →

feat(set_theory/game/nim): Add basic API (#13857)

Estimated changes

Modified src/set_theory/game/nim.lean

modified theorem pgame.nim.exists_move_left_eq

modified theorem pgame.nim.exists_ordinal_move_left_eq

added theorem pgame.nim.left_moves_nim

added theorem pgame.nim.move_left_nim'

added theorem pgame.nim.move_left_nim

added theorem pgame.nim.move_left_nim_heq

added theorem pgame.nim.move_right_nim'

added theorem pgame.nim.move_right_nim

added theorem pgame.nim.move_right_nim_heq

added theorem pgame.nim.neg_nim

added theorem pgame.nim.right_moves_nim

added theorem pgame.nim.to_left_moves_nim_symm_lt

added theorem pgame.nim.to_right_moves_nim_symm_lt