Commit 2021-05-11 07:41 12c9ddf1

View on Github →

feat(set_theory/{pgame, surreal}): add left_distrib_equiv and right_distrib_equiv for pgames (#7440) and several other auxiliary lemmas. Zulip thread

Estimated changes

Modified src/set_theory/game.lean

modified theorem game.le_refl

modified theorem game.le_trans

added theorem game.quot_add

added theorem game.quot_neg

added theorem game.quot_sub

modified def game

Modified src/set_theory/pgame.lean

added theorem pgame.add_right_neg_equiv

added theorem pgame.equiv_of_mk_equiv

added theorem pgame.sub_congr

Modified src/set_theory/surreal.lean

deleted def pgame.add_comm_sub_relabelling

deleted def pgame.add_sub_relabelling

added theorem pgame.left_distrib_equiv

added theorem pgame.left_distrib_equiv_aux'

added theorem pgame.left_distrib_equiv_aux

modified theorem pgame.mul_comm_equiv

modified theorem pgame.mul_zero_equiv

added theorem pgame.right_distrib_equiv

modified theorem pgame.zero_mul_equiv