English
For α finite and n ≥ 2 with n ≤ |α|, the number of permutations whose cycle type is exactly {n} equals (n−1)! times binomial(|α|, n).
Русский
Для конечного α и n ≥ 2 с n ≤ |α| число перестановок с цикловым типом ровно {n} равно (n−1)! умножить на биномиал(|α|, n).
LaTeX
$$$\#\{ g \in \mathrm{Perm}(α) : g.cycleType = \{ n \} \} = (n-1)! \cdot \binom{|α|}{n}$$$
Lean4
/-- The number of cycles of given length -/
theorem card_of_cycleType_singleton {n : ℕ} (hn' : 2 ≤ n) (hα : n ≤ card α) :
#({g | g.cycleType = { n }} : Finset (Perm α)) = (n - 1)! * (choose (card α) n) :=
by
have hn₀ : n ≠ 0 := by omega
have aux : n ! = (n - 1)! * n := by rw [mul_comm, mul_factorial_pred hn₀]
rw [mul_comm, ← Nat.mul_left_inj hn₀, mul_assoc, ← aux, ← Nat.mul_left_inj (factorial_ne_zero _),
Nat.choose_mul_factorial_mul_factorial hα, mul_assoc]
simpa [ite_and, if_pos hα, if_pos hn', mul_comm _ n, mul_assoc] using card_of_cycleType_mul_eq α { n }
