English
The same counting formula as above, phrased for the Finset of permutations with a given cycle type m in Perm α; i.e., the cardinality is the same expression, with the left-hand side reading as the Finset cardinality of {g ∈ Perm α | g.cycleType = m}.
Русский
То же приводимое выше счетное выражение, но примененное к множеству перестановок с заданным цикловым типом m в Perm α; то есть кардинал равен той же формуле.
LaTeX
$$$\#\{ g \in \mathrm{Perm}(\alpha) : g.cycleType = m \} = \begin{cases} \dfrac{|\alpha|!}{((|\alpha| - m.sum)! \cdot m.prod \cdot \prod_{n \in m.toFinset} (m.count n)!)} , & m.sum \le |\alpha| \wedge (\forall a \in m, 2 \le a) \\ 0, & \text{иначе} \end{cases}$$$
Lean4
/-- Cardinality of the `Finset` of `Equiv.Perm α` of given `cycleType` -/
theorem card_of_cycleType (m : Multiset ℕ) :
#({g | g.cycleType = m} : Finset (Perm α)) =
if m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a then
(Fintype.card α)! / ((Fintype.card α - m.sum)! * m.prod * (∏ n ∈ m.toFinset, (m.count n)!))
else 0 :=
by
split_ifs with hm
· -- nonempty case
apply symm
apply Nat.div_eq_of_eq_mul_left
· have : 0 < m.prod := Multiset.prod_pos <| fun a ha => zero_lt_two.trans_le (hm.2 a ha)
positivity
rw [card_of_cycleType_mul_eq, if_pos hm]
· -- empty case
exact (card_of_cycleType_eq_zero_iff α).mpr hm
