mathlib3

95b91b38 - refactor(group_theory/perm/*): disjoint and support in own file (#7450)

refactor(group_theory/perm/*): disjoint and support in own file (#7450) The group_theory/perm/sign file was getting large and too broad in scope. This refactor pulls out `perm.support`, `perm.is_swap`, and `perm.disjoint` into a separate file. A simpler version of #7118.