no goals
α : Type u_1
β : Type ?u.33213
γ : Type ?u.33216
δ : Type ?u.33219
inst✝ : CommMonoid α
p : Multiset α
⊢ Multiset.prod (Multiset.map Associates.mk 0) = Associates.mk (Multiset.prod 0)
simp
no goals
α : Type u_1
β : Type ?u.33213
γ : Type ?u.33216
δ : Type ?u.33219
inst✝ : CommMonoid α
p : Multiset α
a : α
s : Multiset α
ih : Multiset.prod (Multiset.map Associates.mk s) = Associates.mk (Multiset.prod s)
⊢ Multiset.prod (Multiset.map Associates.mk (a ::ₘ s)) = Associates.mk (Multiset.prod (a ::ₘ s))
simp [ih, Associates.mk_mul_mk]