English
If a finite list l of cycles has prod equal to σ and all elements are cycles with pairwise disjoint property, then σ.cycleType equals the mapped lengths.
Русский
Если конечный список l циклов имеет произведение, равное σ, и все элементы являются циклами попарно непересекающимися, то σ.циклТип равен отображению длин.
LaTeX
$$$\forall l : \mathrm{List}(\mathrm{Perm}(\alpha)), (l.\mathrm{prod} = \sigma) → (\forall p \in l, p.IsCycle) → (l.\mathrm Pairwise Disjoint) → \sigma.\mathrmcycleType = l.\mathrm map (\mathrm{Finset.card} \circ \mathrm{support})$$$
Lean4
theorem count_def {σ : Perm α} (n : ℕ) :
σ.cycleType.count n = Fintype.card { c : σ.cycleFactorsFinset // #(c : Perm α).support = n } := by
-- work on the LHS
rw [cycleType, Multiset.count_eq_card_filter_eq]
-- rewrite the `Fintype.card` as a `Finset.card`
rw [Fintype.subtype_card, Finset.univ_eq_attach, Finset.filter_attach', Finset.card_map, Finset.card_attach]
simp only [Function.comp_apply, Finset.card, Finset.filter_val, Multiset.filter_map, Multiset.card_map]
congr 1
apply Multiset.filter_congr
intro d h
simp only [eq_comm, Finset.mem_val.mp h, exists_const]
