English
If a finite set s of cycles gives a noncommutative product equal to σ, then σ.cycleType equals the map of cycle lengths described by s, under the appropriate equivalence.
Русский
Если множество циклов s задаёт произведение, равное σ, то σ.циклТип равняется отображению длин циклов, соответствующих s.
LaTeX
$$$\forall s : \mathrm{Finset}(\mathrm{Perm}(\alpha)), (∀ f ∈ s, f.IsCycle) → (s.\mathrm{toSet}.Pairwise Disjoint) → (s.\mathrm{noncommProd} id (s.\mathrm{Pairwise}.imp Disjoint.commute) = σ) → σ.\mathrmcycleType = s.1.map (\mathrm{Finset.card} \circ \mathrm{support})$$$
Lean4
theorem cycleType_eq {σ : Perm α} (l : List (Perm α)) (h0 : l.prod = σ) (h1 : ∀ σ : Perm α, σ ∈ l → σ.IsCycle)
(h2 : l.Pairwise Disjoint) : σ.cycleType = l.map (Finset.card ∘ support) :=
by
have hl : l.Nodup := nodup_of_pairwise_disjoint_cycles h1 h2
rw [cycleType_eq' l.toFinset]
· simp [List.dedup_eq_self.mpr hl, Function.comp_def]
· simpa using h1
· simpa [hl] using h2
· simp [hl, h0]
