cycleType — Mathlib

English

For IsCycle σ, the cycle type of σ is exactly the singleton consisting of the size of the support of σ.

Русский

Для IsCycle σ цикл-тип σ равен одному элементу: размеру опоры σ.

LaTeX

$$$\forall \sigma : \mathrm{Perm}(\alpha),\; \mathrm{IsCycle}(\sigma) \Rightarrow \sigma.\mathrm{cycleType} = \{\#\sigma.\mathrm{support}\}$$$

Lean4

/-- The cycle type of a permutation -/
def cycleType (σ : Perm α) : Multiset ℕ :=
  σ.cycleFactorsFinset.1.map (Finset.card ∘ support)

Похожие утверждения