mathlib

89196b20 - feat(group_theory/perm/cycle_type): Cycle type of a permutation (#6999)

feat(group_theory/perm/cycle_type): Cycle type of a permutation (#6999) This PR defines the cycle type of a permutation. At some point we should prove the bijection between partitions and conjugacy classes. Co-authored-by: Aaron Anderson <65780815+awainverse@users.noreply.github.com> Co-authored-by: Thomas Browning <tb65536@uw.edu>