Equiv.Perm.exists_with_cycleType_iff

theorem Equiv.Perm.exists_with_cycleType_iff : ∀ (α : Type u_1) [inst : DecidableEq α] [inst_1 : Fintype α] {m : Multiset ℕ}, (∃ g, g.cycleType = m) ↔ m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a

This theorem states that, for any type `α` with decidable equality and finiteness, and any multiset `m` of natural numbers, there exists a permutation `g` whose cycle type is `m` if and only if the sum of the elements in `m` is less than or equal to the number of elements in `α` (given by `Fintype.card α`), and each element `a` in `m` is greater than or equal to 2. In other words, permutations with cycle type `m` exist if and only if the conditions regarding the sum and the individual elements of `m` are satisfied.

More concisely: For any finite type `α` and multiset `m` of natural numbers with sum less than or equal to the cardinality of `α` and each element greater than or equal to 2, there exists a permutation of `α` with cycle type equal to `m`.