Support of a permutation #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
Main definitions #
In the following,
f g : equiv.perm α.
disjoint if their supports are disjoint, i.e.,
every element is fixed either by
f, or by
f.is_swap indicates that the permutation
f is a transposition of two elements.
finset of nonfixed points of a permutation.