Mathlib v3 is deprecated. Go to Mathlib v4

Def game.ordered_add_comm_group_game

Modification history

2022-05-03 16:29
src/set_theory/game/basic.lean
feat(set_theory/game/basic): Inline instances (#13813) …
Deleted game.ordered_add_comm_group_gameView on Github →
2020-04-11 04:27
src/set_theory/game.lean
chore(*): switch to lean 3.8.0 (#2361) …
Added game.ordered_add_comm_group_gameView on Github →