*): remove `relabelling`
#18518

Open

refactor(set_theory/game/*): remove `relabelling` #18518

astrainfinita wants to merge 12 commits into master from FR_game_relabelling

feat(set_theory/game/pgame): define `pgame.identical`

855fd1cd

docs, protected

1b3d193b

mem mul

fe396470

mul_comm

415aea22

`identical_zero` `identical.sub`

d2e5ec35

golf

f61ce93f

more lemmas

371fefb3

fix

307fe760

`one_mul` `mul_one`

ec638b9e

no they are lemmas

a0da9565

inv lemmas

178d7013

refactor(set_theory/game/*): remove `relabelling`

e91c4253

astrainfinita added WIP

astrainfinita changed the title ~~refactor(set_theory/game/*): remove relabelling~~ refactor(set_theory/game/*): remove `relabelling` 2 years ago

mathlib-dependent-issues-bot added blocked-by-other-PR

kim-em added too-late

mathlib-dependent-issues-bot removed blocked-by-other-PR

Reviewers

No reviews

Assignees

No one assigned

Labels

WIP too-late

Milestone

No milestone