sum_cycleType — Mathlib

English

The sum of the cycle lengths equals the size of the support of the permutation: cycleType(σ).sum = |σ.support|.

Русский

Сумма длин циклов равна размеру множества подстановки: cycleType(σ).sum = |σ.support|.

LaTeX

$$$$\mathrm{cycleType}(\sigma).sum = |\sigma.\mathrm{support}|.$$$$

Lean4

theorem sum_cycleType (σ : Perm α) : σ.cycleType.sum = #σ.support := by
  induction σ using cycle_induction_on with
  | base_one => simp
  | base_cycles σ hσ => rw [hσ.cycleType, Multiset.sum_singleton]
  | induction_disjoint σ τ hd _ hσ hτ => rw [hd.cycleType_mul, sum_add, hσ, hτ, hd.card_support_mul]

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