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 List.exists_pw_disjoint_with_card {α : Type u_2} [Fintype α] {c : List ℕ} (hc : c.sum ≤ Fintype.card α) : ∃ (o : List (List α)), map length o = c ∧ (∀ s ∈ o, s.Nodup) ∧ Pairwise Disjoint o

For any c : List ℕ whose sum is at most Fintype.card α, we can find o : List (List α) whose members have no duplicate, whose lengths given by c, and which are pairwise disjoint

theorem Equiv.Perm.exists_with_cycleType_iff (α : Type u_1) [DecidableEq α] [Fintype α] {m : Multiset ℕ} : (∃ (g : 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.