Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-29 14:43 966b3b18

View on Github →

feat(set_theory/{surreal, pgame}): mul_comm for surreal numbers (#7376) This PR adds a proof of commutativity of multiplication for surreal numbers. We also add mul_zero and zero_mul along with several useful lemmas. Finally, this renames a handful of lemmas about relabelling in order to enable dot notation. Zulip thread

Estimated changes

Modified src/set_theory/game/impartial.lean

Modified src/set_theory/pgame.lean

deleted theorem pgame.equiv_of_relabelling

deleted theorem pgame.le_of_relabelling

deleted theorem pgame.le_of_restricted

added def pgame.relabelling.add_congr

added theorem pgame.relabelling.equiv

added theorem pgame.relabelling.le

added def pgame.relabelling.neg_congr

added def pgame.relabelling.restricted:

added def pgame.relabelling.sub_congr

added theorem pgame.restricted.le

deleted def pgame.restricted_of_relabelling

Modified src/set_theory/surreal.lean

added def pgame.add_comm_sub_relabelling

added def pgame.add_sub_relabelling

added def pgame.left_moves_mul

added theorem pgame.mk_mul_move_left_inl

added theorem pgame.mk_mul_move_left_inr

added theorem pgame.mk_mul_move_right_inl

added theorem pgame.mk_mul_move_right_inr

added theorem pgame.mul_comm_equiv

added def pgame.mul_comm_relabelling

added theorem pgame.mul_move_left_inl

added theorem pgame.mul_move_left_inr

added theorem pgame.mul_move_right_inl

added theorem pgame.mul_move_right_inr

added theorem pgame.mul_zero_equiv

added def pgame.mul_zero_relabelling

added def pgame.right_moves_mul

added theorem pgame.zero_mul_equiv

added def pgame.zero_mul_relabelling