Commit 2022-06-16 22:34 d0b93faf

View on Github →

feat(set_theory/{pgame, basic}): Notation for relabelling, golfing (#14155) We introduce the notation ≡r for relabellings between two pre-games. We also golf many theorems on relabellings.

Estimated changes

Modified src/set_theory/game/basic.lean

modified theorem pgame.mul_zero_equiv

modified def pgame.mul_zero_relabelling

modified theorem pgame.zero_mul_equiv

modified def pgame.zero_mul_relabelling

Modified src/set_theory/game/birthday.lean

modified theorem pgame.relabelling.birthday_congr

Modified src/set_theory/game/impartial.lean

modified theorem pgame.impartial.impartial_congr

Modified src/set_theory/game/nim.lean

modified def pgame.nim.nim_zero_relabelling

Modified src/set_theory/game/pgame.lean

modified def pgame.add_assoc_relabelling

modified def pgame.add_comm_relabelling

modified def pgame.add_zero_relabelling

modified theorem pgame.equiv.is_empty

modified def pgame.neg_add_relabelling

modified def pgame.relabel

modified def pgame.relabelling.add_congr

modified theorem pgame.relabelling.equiv

added theorem pgame.relabelling.ge

modified def pgame.relabelling.is_empty

modified theorem pgame.relabelling.le

modified def pgame.relabelling.neg_congr

modified def pgame.relabelling.refl

modified def pgame.relabelling.restricted

modified def pgame.relabelling.sub_congr

modified def pgame.relabelling.symm

modified def pgame.relabelling.trans

added def pgame.restricted.trans

modified def pgame.zero_add_relabelling