Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-17 00:02 84a27d60

View on Github →

feat(set_theory/game): add mul_one and mul_assoc for pgames (#7610) and several simp lemmas. I also simplified some of the existing proofs using rw and simp and made them easier to read. This is the final PR for multiplication of pgames (hopefully)! Next step: prove numeric_mul and define multiplication for surreal.

Estimated changes

Modified src/set_theory/game.lean

deleted theorem game.quot_add

deleted theorem game.quot_neg

deleted theorem game.quot_sub

modified theorem pgame.left_distrib_equiv

deleted theorem pgame.left_distrib_equiv_aux'

deleted theorem pgame.left_distrib_equiv_aux

added theorem pgame.mul_assoc_equiv

deleted def pgame.mul_comm_relabelling

added theorem pgame.mul_one_equiv

added theorem pgame.one_mul_equiv

added theorem pgame.quot_add

added theorem pgame.quot_eq_of_mk_quot_eq

added theorem pgame.quot_left_distrib

added theorem pgame.quot_left_distrib_sub

added theorem pgame.quot_mul_assoc

added theorem pgame.quot_mul_comm

added theorem pgame.quot_mul_neg

added theorem pgame.quot_mul_one

added theorem pgame.quot_mul_zero

added theorem pgame.quot_neg

added theorem pgame.quot_neg_mul

added theorem pgame.quot_one_mul

added theorem pgame.quot_right_distrib

added theorem pgame.quot_right_distrib_sub

added theorem pgame.quot_sub

added theorem pgame.quot_zero_mul