Commit 2024-09-18 07:39 f518a558
View on Github →feat: lemmas on permutations, cycles, etc. (#9602)
This PR establishes various lemmas in the theory of permutation groups,
pertaining to the supports, cycle decompositions, and the conjugation action
of ConjAct (Equiv.Perm α) on Equiv.Perm α
This lemmas stem out PR #9359 and are used there to compute the cardinalities
of the conjugacy classes of permutations.