Commit 2021-05-14 14:25 2373ee62

View on Github →

refactor(set_theory/{surreal, game}): move mul from surreal to game (#7580) The next step is to provide several simp lemmas for multiplication of pgames in terms of games. None of these statements involve surreal numbers.

Estimated changes

Modified src/set_theory/game.lean

added def pgame.inv'

added inductive pgame.inv_ty

added def pgame.inv_val

added theorem pgame.left_distrib_equiv

added theorem pgame.left_distrib_equiv_aux'

added theorem pgame.left_distrib_equiv_aux

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 def pgame.mul

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 theorem pgame.right_distrib_equiv

added def pgame.right_moves_mul

added theorem pgame.zero_mul_equiv

added def pgame.zero_mul_relabelling

Modified src/set_theory/surreal.lean

deleted def pgame.inv'

deleted inductive pgame.inv_ty

deleted def pgame.inv_val

deleted theorem pgame.left_distrib_equiv

deleted theorem pgame.left_distrib_equiv_aux'

deleted theorem pgame.left_distrib_equiv_aux

deleted def pgame.left_moves_mul

deleted theorem pgame.mk_mul_move_left_inl

deleted theorem pgame.mk_mul_move_left_inr

deleted theorem pgame.mk_mul_move_right_inl

deleted theorem pgame.mk_mul_move_right_inr

deleted def pgame.mul

deleted theorem pgame.mul_comm_equiv

deleted def pgame.mul_comm_relabelling

deleted theorem pgame.mul_move_left_inl

deleted theorem pgame.mul_move_left_inr

deleted theorem pgame.mul_move_right_inl

deleted theorem pgame.mul_move_right_inr

deleted theorem pgame.mul_zero_equiv

deleted def pgame.mul_zero_relabelling

deleted theorem pgame.right_distrib_equiv

deleted def pgame.right_moves_mul

deleted theorem pgame.zero_mul_equiv

deleted def pgame.zero_mul_relabelling