mathlib3

c088f657 - chore(data/equiv/perm): Move around lemmas about perm and swap (#5153)

chore(data/equiv/perm): Move around lemmas about perm and swap (#5153) Only a very small fraction of `data/equiv/basic` needs knowledge of groups, moving out `perm_group` lets us cut the dependency. The new `perm_group` file is then a good place for some of the lemmas in `group_theory/perm/sign`, especially those which just restate `equiv` lemmas in terms of `*` and `⁻¹` instead of `.trans` and `.symm`. This moves a few lemmas about swap out of the `equiv.perm` namespace and into `equiv`, since `equiv.swap` is also in that namespace.