Commit 2022-04-21 17:29 b7cba576

View on Github →

chore(set_theory/game/*): Protect ambiguous lemmas (#13557) Protect pgame.neg_zero and inline pgame.add_le_add_left and friends into covariant_class instances.

Estimated changes

Modified src/set_theory/game/basic.lean

deleted theorem game.add_le_add_left

Modified src/set_theory/game/impartial.lean

Modified src/set_theory/game/pgame.lean

deleted theorem pgame.add_le_add_left

deleted theorem pgame.add_le_add_right

deleted theorem pgame.add_lt_add_left

deleted theorem pgame.add_lt_add_right

deleted theorem pgame.neg_neg

deleted theorem pgame.neg_zero

deleted def pgame.relabelling.restricted:

added def pgame.relabelling.restricted

deleted theorem pgame.zero_lt_half

Modified src/set_theory/surreal/basic.lean

Modified src/set_theory/surreal/dyadic.lean