ι : Type ?u.997971
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : CommMonoid α
s : Multiset (Additive α)
⊢ Multiset.sum s = Multiset.prod s
ι : Type ?u.997971
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : CommMonoid α
s : Multiset (Additive α)
⊢ ↑toMul (Multiset.sum s) = Multiset.prod (Multiset.map (↑toMul) s)
simp [toMul, ofMul]
no goals
ι : Type ?u.997971
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : CommMonoid α
s : Multiset (Additive α)
⊢ Multiset.sum s = Multiset.prod s
rfl