English
Given a finite set of cycles s whose elements are cycles, pairwise disjoint, and whose noncommutative product equals σ, the cycle type of σ equals the map of cycle lengths corresponding to s.
Русский
Для конечного множества циклов s состоящего из циклов, попарно непересекающихся, чьи произведения дают σ, цикл-тип σ равен отображению длин этих циклов.
LaTeX
$$$\forall s : \mathrm{Finset}(\mathrm{Perm}(\alpha)), (\forall f \in s, f.IsCycle) \to (s.\mathrm{Set}.Pairwise \mathrm{Disjoint}) \to (s.\mathrm{noncommProd} id (s.\mathrm{disjoint'} ) = \sigma) \Rightarrow \sigma.\mathrm{cycleType} = s.1.map (\mathrm{Finset.card} \circ \mathrm{support})$$$
Lean4
theorem cycleType_def (σ : Perm α) : σ.cycleType = σ.cycleFactorsFinset.1.map (Finset.card ∘ support) :=
rfl
