Possible cycle types of permutations #

theorem Equiv.Perm.exists_with_cycleType_iff (α : Type u_1) [DecidableEq α] [Fintype α] {m : Multiset } :
(∃ (g : Equiv.Perm α), Equiv.Perm.cycleType g = m) Multiset.sum m Fintype.card α am, 2 a

There are permutations with cycleType m if and only if its sum is at most Fintype.card α and its members are at least 2.