Commit 2020-12-01 13:25 c088f657

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.