nim}): Minimum excluded ordinal (#12659)

Commit

3 years ago

feat(set_theory/{ordinal_arithmetic, game/nim}): Minimum excluded ordinal (#12659) We define `mex` and `bmex`, and use the former to golf the proof of Sprague-Grundy.

Author

vihdzp

Parents

5fcad214

mathlib3 5fb7b7b6 - feat(set_theory/{ordinal_arithmetic, game/nim}): Minimum excluded ordinal (#12659)

mathlib3
5fb7b7b6 - feat(set_theory/{ordinal_arithmetic, game/nim}): Minimum excluded ordinal (#12659)