ι : Type u_1
α : Type u_3
β : Type u_2
inst✝³ : DecidableEq α
inst✝² : Semiring α
inst✝¹ : AddCommMonoid β
inst✝ : Module α β
s : Finset ι
σ : Perm ι
hσ : IsCycleOn σ ↑s
f : ι → α
g : ι → β
⊢ ∑ x in range (card s),
      ∑ x_1 in s,
        f
            (↑{ toFun := fun i => (i, ↑(σ ^ x) i),
                    inj' :=
                      (_ :
                        ∀ (i j : ι),
                          (fun i => (i, ↑(σ ^ x) i)) i = (fun i => (i, ↑(σ ^ x) i)) j →
                            ((fun i => (i, ↑(σ ^ x) i)) i).fst = ((fun i => (i, ↑(σ ^ x) i)) j).fst) }
                x_1).fst •
          g
            (↑{ toFun := fun i => (i, ↑(σ ^ x) i),
                    inj' :=
                      (_ :
                        ∀ (i j : ι),
                          (fun i => (i, ↑(σ ^ x) i)) i = (fun i => (i, ↑(σ ^ x) i)) j →
                            ((fun i => (i, ↑(σ ^ x) i)) i).fst = ((fun i => (i, ↑(σ ^ x) i)) j).fst) }
                x_1).snd =
    ∑ x in range (card s), ∑ x_1 in s, f x_1 • g (↑(σ ^ x) x_1)
ι : Type u_1
α : Type u_3
β : Type u_2
inst✝³ : DecidableEq α
inst✝² : Semiring α
inst✝¹ : AddCommMonoid β
inst✝ : Module α β
s : Finset ι
σ : Perm ι
hσ : IsCycleOn σ ↑s
f : ι → α
g : ι → β
⊢ (∑ i in s, f i) • ∑ i in s, g i = ∑ k in range (card s), ∑ i in s, f i • g (↑(σ ^ k) i)
simp_rw [sum_smul_sum, product_self_eq_disjUnion_perm hσ, sum_disjiUnion, sum_map]
no goals
ι : Type u_1
α : Type u_3
β : Type u_2
inst✝³ : DecidableEq α
inst✝² : Semiring α
inst✝¹ : AddCommMonoid β
inst✝ : Module α β
s : Finset ι
σ : Perm ι
hσ : IsCycleOn σ ↑s
f : ι → α
g : ι → β
⊢ ∑ x in range (card s),
      ∑ x_1 in s,
        f
            (↑{ toFun := fun i => (i, ↑(σ ^ x) i),
                    inj' :=
                      (_ :
                        ∀ (i j : ι),
                          (fun i => (i, ↑(σ ^ x) i)) i = (fun i => (i, ↑(σ ^ x) i)) j →
                            ((fun i => (i, ↑(σ ^ x) i)) i).fst = ((fun i => (i, ↑(σ ^ x) i)) j).fst) }
                x_1).fst •
          g
            (↑{ toFun := fun i => (i, ↑(σ ^ x) i),
                    inj' :=
                      (_ :
                        ∀ (i j : ι),
                          (fun i => (i, ↑(σ ^ x) i)) i = (fun i => (i, ↑(σ ^ x) i)) j →
                            ((fun i => (i, ↑(σ ^ x) i)) i).fst = ((fun i => (i, ↑(σ ^ x) i)) j).fst) }
                x_1).snd =
    ∑ x in range (card s), ∑ x_1 in s, f x_1 • g (↑(σ ^ x) x_1)
rfl