Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-06 07:48 4b788397

View on Github →

feat(set_theory/game/basic): generalize equivalences to relabellings (#15252) This PR does the following:

Generalize quot_mul_comm, quot_neg_mul, quot_mul_neg, quot_mul_one, quot_one_mul from pre-game equivalences to relabellings.
Add a bunch of dsimp lemmas, used in neg_mul_relabelling.
Heavily golf the corresponding proofs.
Uncontroversial spacing and parentheses fixes.

Estimated changes

Modified src/set_theory/game/basic.lean

added def pgame.mul_comm_relabelling

added def pgame.mul_neg_relabelling

modified theorem pgame.mul_one_equiv

added def pgame.mul_one_relabelling

added theorem pgame.neg_mk_mul_move_left_inl

added theorem pgame.neg_mk_mul_move_left_inr

added theorem pgame.neg_mk_mul_move_right_inl

added theorem pgame.neg_mk_mul_move_right_inr

added def pgame.neg_mul_relabelling

modified theorem pgame.one_mul_equiv

added def pgame.one_mul_relabelling

modified theorem pgame.quot_mul_comm

modified theorem pgame.quot_mul_one

modified theorem pgame.quot_neg_mul

modified theorem pgame.quot_one_mul