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