filter_parts_partition_eq_cycleType

English

Let σ be a permutation of a finite set α. The multiset of cycle lengths of σ, excluding 1-cycles, equals the cycle type of σ.

Русский

Пусть σ — перестановка на конечном множестве α. Мультисет длин цикла σ, исключая 1-цикл, совпадает с типом цикла σ.

LaTeX

$$$((\operatorname{partition}(\sigma)).parts)_{\ge 2} = \sigma.cycleType$$$

Lean4

theorem filter_parts_partition_eq_cycleType {σ : Perm α} : ((partition σ).parts.filter fun n => 2 ≤ n) = σ.cycleType :=
  by
  rw [parts_partition, filter_add, Multiset.filter_eq_self.2 fun _ => two_le_of_mem_cycleType,
    Multiset.filter_eq_nil.2 fun a h => ?_, add_zero]
  rw [Multiset.eq_of_mem_replicate h]
  decide

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