mathlib

d0b93faf - feat(set_theory/{pgame, basic}): Notation for `relabelling`, golfing (#14155)

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.