cycleType_mul — Mathlib

English

If two permutations σ and τ are disjoint, then the cycle-type of their product equals the sum of their cycle-types.

Русский

Если перестановки σ и τ не влияют друг на друга (они несовместны), то цикл-тип произведения στ равен сумме цикл-типов σ и τ.

LaTeX

$$$$\text{Disjoint}(\sigma,\tau) \implies (\sigma\tau).\mathrm{cycleType} = \sigma.\mathrm{cycleType} + \tau.\mathrm{cycleType}.$$$$

Lean4

theorem cycleType_mul {σ τ : Perm α} (h : Disjoint σ τ) : (σ * τ).cycleType = σ.cycleType + τ.cycleType :=
  by
  rw [cycleType_def, cycleType_def, cycleType_def, h.cycleFactorsFinset_mul_eq_union, ← Multiset.map_add,
    Finset.union_val, Multiset.add_eq_union_iff_disjoint.mpr _]
  exact Finset.disjoint_val.2 h.disjoint_cycleFactorsFinset

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