ι : Type ?u.321448
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : CommMonoid β
⊢ ∏ x in s, f x * g x = fold (fun x x_1 => x * x_1) 1 (fun x => f x * g x) s
ι : Type ?u.321448
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : CommMonoid β
⊢ ∏ x in s, f x * g x = fold (fun x x_1 => x * x_1) (1 * 1) (fun x => f x * g x) s
rw [one_mul]
no goals
ι : Type ?u.321448
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : CommMonoid β
⊢ ∏ x in s, f x * g x = fold (fun x x_1 => x * x_1) 1 (fun x => f x * g x) s
rfl