In the following, f g : equiv.perm α.
f g : equiv.perm α
f = swap x y
x ≠ y
x : α
Two permutations f and g are disjoint if their supports are disjoint, i.e.,
every element is fixed either by f, or by g.
f.is_swap indicates that the permutation f is a transposition of two elements.
The finset of nonfixed points of a permutation.