no goals
ι : Type u_2
α : Type u_1
β : Type ?u.111733
γ : Type ?u.111736
inst✝ : NonUnitalNonAssocSemiring α
a : α
s : Multiset ι
f : ι → α
⊢ sum (map (fun i => a * f i) 0) = a * sum (map f 0)
simp
no goals
ι : Type u_2
α : Type u_1
β : Type ?u.111733
γ : Type ?u.111736
inst✝ : NonUnitalNonAssocSemiring α
a : α
s✝ : Multiset ι
f : ι → α
i : ι
s : Multiset ι
ih : sum (map (fun i => a * f i) s) = a * sum (map f s)
⊢ sum (map (fun i => a * f i) (i ::ₘ s)) = a * sum (map f (i ::ₘ s))
simp [ih, mul_add]