no goals
α : Type u_1
β : Type ?u.186829
ι : Type ?u.186832
G : Type ?u.186835
M : Type u_2
N : Type ?u.186841
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
hf : Set.Finite (mulSupport f)
⊢ (∏ᶠ (i : α), f i) = ∏ i in Finite.toFinset hf, f i
classical rw [finprod_def, dif_pos hf]
no goals
α : Type u_1
β : Type ?u.186829
ι : Type ?u.186832
G : Type ?u.186835
M : Type u_2
N : Type ?u.186841
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
hf : Set.Finite (mulSupport f)
⊢ (∏ᶠ (i : α), f i) = ∏ i in Finite.toFinset hf, f i
rw [finprod_def, dif_pos hf]