sum_smul_sum_eq_sum_perm — Mathlib

English

For a cycle f on a finite set s, the self product over s equals a disjoint union of diagonals along powers of f.

Русский

Для цикла f над конечным множеством s произведение по s разложимо на дизъюнкты диагоналей вдоль степеней f.

LaTeX

$$For hf : f.IsCycleOn s, $$ \prod_{i \in s} i = \bigcup_{k=0}^{|s|-1} s.map (a \mapsto (a, f^k(a))) $$$$

Lean4

theorem sum_smul_sum_eq_sum_perm (hσ : σ.IsCycleOn s) (f : ι → α) (g : ι → β) :
    (∑ i ∈ s, f i) • ∑ i ∈ s, g i = ∑ k ∈ range #s, ∑ i ∈ s, f i • g ((σ ^ k) i) :=
  by
  rw [sum_smul_sum, ← sum_product']
  simp_rw [product_self_eq_disjiUnion_perm hσ, sum_disjiUnion, sum_map, Embedding.coeFn_mk]

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