English
For a general multiset m, the number of even permutations in the alternating group with cycleType m is given by a piecewise factorial formula, zero when the type is not realizable by an even permutation under the given cardinality constraints.
Русский
Для произвольного мультiset m число чётных перестановок с cycleType m рассчитывается по формуле, состоящей из факториалов; ноль, если такой тип не может быть реализацией чётной перестановки при данных размерах множества.
LaTeX
$$$\#\{ g\in alternatingGroup(\alpha) : (g : Perm \alpha).cycleType = m \} = \begin{cases} \frac{|\alpha|!}{(|\alpha| - m.sum)! \; (m.prod) \; (\prod_{n \in m.toFinset} (m.count n)!)} , & \text{(conditions with parity and bounds)} \\\ 0, & \text{otherwise} \end{cases}$$$
Lean4
/-- The cardinality of even permutations of given `cycleType` -/
theorem card_of_cycleType (m : Multiset ℕ) :
#{g : alternatingGroup α | (g : Equiv.Perm α).cycleType = m} =
if (m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (m.sum + Multiset.card m) then
(Fintype.card α)! / ((Fintype.card α - m.sum)! * (m.prod * (∏ n ∈ m.toFinset, (m.count n)!)))
else 0 :=
by
split_ifs with hm
· -- m is an even cycle_type
rw [← Finset.card_map, map_subtype_of_cycleType, if_pos hm.2, Equiv.Perm.card_of_cycleType α m, if_pos hm.1,
mul_assoc]
· -- m does not correspond to a permutation, or to an odd one,
rw [← Finset.card_map, map_subtype_of_cycleType]
rw [apply_ite Finset.card, Finset.card_empty]
split_ifs with hm'
· rw [Equiv.Perm.card_of_cycleType, if_neg]
obtain hm | hm := not_and_or.mp hm
· exact hm
· contradiction
· rfl
