English
For n ≥ 2, and n ≤ |α|, the number of even permutations with cycleType {n} equals (n-1)! * C(|α|, n) if n is odd, otherwise 0.
Русский
Пусть n ≥ 2 и n ≤ |α|. Число чётных перестановок с cycleType {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 number of cycles of given length -/
theorem card_of_cycleType_singleton {n : ℕ} (hn : 2 ≤ n) (hα : n ≤ card α) :
#{g : alternatingGroup α | g.val.cycleType = { n }} = if Odd n then (n - 1)! * (choose (card α) n) else 0 :=
by
rw [← card_map, map_subtype_of_cycleType, apply_ite Finset.card]
simp only [Multiset.sum_singleton, Multiset.card_singleton, Finset.card_empty]
simp_rw [← Nat.not_odd_iff_even, Nat.odd_add_one, not_not, Perm.card_of_cycleType_singleton hn hα]
