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