Theorem: DividedPowerAlgebra.dp_sum_smul (DividedPowers/DPAlgebra/Init.lean)

State before:
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : DecidableEq ι
s : Finset ι
q : ℕ
a : ι → R
x : ι → M
⊢ dp R q (∑ i ∈ s, a i • x i) =
    ∑ k ∈ s.sym q, (∏ i ∈ s, a i ^ Multiset.count i ↑k) • ∏ i ∈ s, dp R (Multiset.count i ↑k) (x i)
Tactic:
simp_rw [dp_sum, dp_smul, Algebra.smul_def, map_prod, ← Finset.prod_mul_distrib]
State after:
no goals