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 α), g.cycleType = m) ↔ m.sum ≤ 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.