Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-03 16:29 86887539

View on Github →

feat(set_theory/game/basic): Inline instances (#13813) We also add a few missing instances.

Estimated changes

Modified src/set_theory/game/basic.lean

deleted def game.add

deleted theorem game.add_assoc

deleted theorem game.add_comm

deleted theorem game.add_left_neg

deleted theorem game.add_zero

deleted def game.game_partial_order

deleted def game.le

deleted def game.lt

deleted def game.neg

modified theorem game.not_le

added theorem game.not_lt

added def game.ordered_add_comm_group

deleted def game.ordered_add_comm_group_game

added def game.partial_order

deleted theorem game.zero_add

deleted def pgame.mul