swap_factors represents a permutation as a product of a list of transpositions. The representation is non unique and depends on the linear order structure. For types without linear order trunc_swap_factors can be used

set of all pairs (⟨a, b⟩ : Σ a : fin n, fin n) such that b < a

sign of a permutation returns the signature or parity of a permutation, 1 for even permutations, -1 for odd permutations. It is the unique surjective group homomorphism from perm α to the group with two elements.