English
For a finite α and a multiset m of cycle lengths, the number of permutations g ∈ Perm α with cycle type m is given by the standard multinomial formula: if s = m.sum satisfies s ≤ |α| and every element of m is at least 2, then the count is |α|! divided by (|α|−s)! times the product of the cycle lengths, times the factorials of the multiplicities of the lengths. If not, the count is 0.
Русский
Для конечного множества α и мультисета m длин циклов количество перестановок g в Perm α с цикловым типом m равно стандартной формуле: если s = m.sum удовлетворяет s ≤ |α| и каждый элемент m не меньше 2, то число равно |α|! делить на (|α|−s)! умножить на произведение длин циклов и на факториалы частот повторений длин. Иначе число равно 0.
LaTeX
$$$\#({g \mid g.cycleType = m} : Finset (Perm α)) = \begin{cases} \dfrac{(|α|)!}{((|α| - m.sum)! \cdot m.prod \cdot \prod_{n \in m.toFinset} (m.count n)!)} , & m.sum \le |α| \wedge (\forall a \in m, 2 \le a) \\ 0, & \text{иначе} \end{cases}$$$
Lean4
theorem card_of_cycleType_mul_eq (m : Multiset ℕ) :
#({g | g.cycleType = m} : Finset (Perm α)) *
((Fintype.card α - m.sum)! * m.prod * (∏ n ∈ m.toFinset, (m.count n)!)) =
if (m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) then (Fintype.card α)! else 0 :=
by
split_ifs with hm
· -- nonempty case
classical
obtain ⟨g, rfl⟩ := (exists_with_cycleType_iff α).mpr hm
convert card_isConj_mul_eq g
simp_rw [Set.coe_setOf, Nat.card_eq_fintype_card, ← Fintype.card_coe, Finset.mem_filter, Finset.mem_univ, true_and,
← isConj_iff_cycleType_eq, isConj_comm (g := g)]
· -- empty case
rw [(card_of_cycleType_eq_zero_iff α).mpr hm, zero_mul]
