English
If σ is the product of a list of pairwise disjoint cycles and each is a cycle, then σ.cycleType equals the image of the list of cycles under card ∘ support.
Русский
Если σ — произведение упорядоченного списка попарно непересекающихся циклов, и каждый элемент списка — цикл, то σ.циклТип равен образу списка циклов под card ∘ support.
LaTeX
$$$\forall l : \mathrm{List}(\mathrm{Perm}(\alpha)), (l.\mathrm{prod} = \sigma) \to (\forall x \in l, x.IsCycle) \to (l.\mathrm{Pairwise} Disjoint) \to \sigma.\mathrmcycleType = l.1.map (\mathrm{Finset.card} \circ \mathrm{support})$$$
Lean4
theorem cycleType_eq' {σ : Perm α} (s : Finset (Perm α)) (h1 : ∀ f : Perm α, f ∈ s → f.IsCycle)
(h2 : (s : Set (Perm α)).Pairwise Disjoint) (h0 : s.noncommProd id (h2.imp fun _ _ => Disjoint.commute) = σ) :
σ.cycleType = s.1.map (Finset.card ∘ support) :=
by
rw [cycleType_def]
congr
rw [cycleFactorsFinset_eq_finset]
exact ⟨h1, h2, h0⟩
