English
The number of even permutations with cycleType {n} is (n-1)! * C(card α, n) if n is odd, and 0 if n is even.
Русский
Число чётных перестановок с циклическим типом {n} равно (n-1)! ⋅ C(|α|, n) если n нечётно, иначе 0.
LaTeX
$$$\#\{ g\in alternatingGroup(\alpha) : (g : Perm \alpha).cycleType = {n} \} = \begin{cases} (n-1)! \cdot {card(\alpha) \choose n}, & \text{Odd}(n) \\\ 0, & \text{Else} \end{cases}$$$
Lean4
/-- The cardinality of even permutations of given `cycleType` -/
theorem card_of_cycleType_mul_eq (m : Multiset ℕ) :
#{g : alternatingGroup α | g.val.cycleType = m} *
((Fintype.card α - m.sum)! * m.prod * (∏ n ∈ m.toFinset, (m.count n)!)) =
if ((m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (m.sum + Multiset.card m)) then (Fintype.card α)! else 0 :=
by
rw [← Finset.card_map, map_subtype_of_cycleType, apply_ite Finset.card, Finset.card_empty, ite_mul, zero_mul]
simp only [and_comm (b := Even _)]
rw [ite_and, Equiv.Perm.card_of_cycleType_mul_eq]
