Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-22 10:07 011a2622

View on Github →

feat(set_theory/game): impartial games and the Sprague-Grundy theorem (#3855)

Estimated changes

added def pgame.impartial
added theorem pgame.impartial_add
added theorem pgame.impartial_def
added theorem pgame.impartial_neg
added theorem pgame.zero_impartial
added theorem nim.Grundy_value_def
added theorem nim.Sprague_Grundy
added theorem nim.nim_def
added theorem nim.nim_impartial
added theorem nim.nim_wf_lemma
added def nim.nonmoves
added theorem nim.nonmoves_nonempty
added def nim
added def ordinal.out
added theorem ordinal.type_out'
added def pgame.first_wins
added def pgame.left_wins
added theorem pgame.omega_left_wins
added theorem pgame.one_left_wins
added def pgame.right_wins
added theorem pgame.star_first_wins
added theorem pgame.winner_cases
added theorem pgame.zero_first_loses