ι : Type ?u.1000663
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : AddCommMonoid α
s : Multiset (Multiplicative α)
⊢ Multiset.prod s = Multiset.sum s
ι : Type ?u.1000663
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : AddCommMonoid α
s : Multiset (Multiplicative α)
⊢ ↑toAdd (Multiset.prod s) = Multiset.sum (Multiset.map (↑toAdd) s)
simp [toAdd, ofAdd]
no goals
ι : Type ?u.1000663
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : AddCommMonoid α
s : Multiset (Multiplicative α)
⊢ Multiset.prod s = Multiset.sum s
rfl