Commit 2025-02-01 07:23 05f71fad
View on Github →feat(GroupTheory/Perm/Centralizer): study the centralizer of a permutation (#17522)
This is the core of the work on the centralizer of a permutation.
It is the sequel of several PR which lay out basic useful results.
Let α : Type with Fintype α (and DecidableEq α).
The main goal of this file is to compute the cardinality of
conjugacy classes in Equiv.Perm α.
Every g : Equiv.Perm α has a cycleType α : Multiset ℕ.
By Equiv.Perm.isConj_iff_cycleType_eq,
two permutations are conjugate in Equiv.Perm α iff
their cycle types are equal.
To compute the cardinality of the conjugacy classes, we could use
a purely combinatorial approach and compute the number of permutations
with given cycle type but we resorted to a more algebraic approach.
A subsequent PR #17047 treats the case of the alternating group.