cycleType — Mathlib

English

For an IsCycle permutation σ, its cycle type equals the singleton containing the size of the support.

Русский

Для IsCycle перестановки σ цикл-тип равен одиночному множеству, содержащему размер опоры σ.

LaTeX

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

Lean4

theorem cycleType {σ : Perm α} (hσ : IsCycle σ) : σ.cycleType = {#σ.support} :=
  cycleType_eq [σ] (mul_one σ) (fun _τ hτ => (congr_arg IsCycle (List.mem_singleton.mp hτ)).mpr hσ)
    (List.pairwise_singleton Disjoint σ)

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