def SymmetricGroups.cycleType {α : Type u_1} [Fintype α] [DecidableEq α] (σ : Equiv.Perm α) : Multiset ℕ

theorem SymmetricGroups.conjugate_iff_same_cycleType {n : ℕ} {σ τ : Equiv.Perm (Fin n)} : IsConj σ τ ↔ σ.cycleType = τ.cycleType