# Possible cycle types of permutations #

- For
`m : Multiset ℕ`

,`Equiv.Perm.exists_with_cycleType_iff m`

proves that there are permutations with cycleType`m`

if and only if its sum is at most`Fintype.card α`

and its members are at least 2.

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 α ∧ ∀ a ∈ m, 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.