mathlib3

6e836c43 - feat(group_theory/perm/{cycles, cycle_type}): permutations are conjugate iff they have the same cycle type (#7335)

feat(group_theory/perm/{cycles, cycle_type}): permutations are conjugate iff they have the same cycle type (#7335) Slightly strengthens the induction principle `equiv.perm.cycle_induction_on` Proves that two permutations are conjugate iff they have the same cycle type: `equiv.perm.is_conj_iff_cycle_type_eq` Co-authored-by: Aaron Anderson <65780815+awainverse@users.noreply.github.com> Co-authored-by: Thomas Browning <tb65536@uw.edu>