mathlib3

7cebe816 - A group element induces a graph isomorphism; and if the group is infinite, such isomorphisms can be used to move finsets to disjoint images