α : Type u_1
β : Type ?u.217456
ι : Type ?u.217459
G : Type ?u.217462
M : Type u_2
N : Type ?u.217468
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Set α
hf : Set.Finite (mulSupport (mulIndicator s f))
hg : Set.Finite (mulSupport (mulIndicator s g))
⊢ (∏ᶠ (i : α) (_ : i ∈ s), f i * g i) = (∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ s), g i
α : Type u_1
β : Type ?u.217456
ι : Type ?u.217459
G : Type ?u.217462
M : Type u_2
N : Type ?u.217468
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Set α
hf : Set.Finite (s ∩ mulSupport f)
hg : Set.Finite (s ∩ mulSupport g)
⊢ (∏ᶠ (i : α) (_ : i ∈ s), f i * g i) = (∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ s), g i
rw [← mulSupport_mulIndicator] at hf hg
no goals
α : Type u_1
β : Type ?u.217456
ι : Type ?u.217459
G : Type ?u.217462
M : Type u_2
N : Type ?u.217468
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Set α
hf : Set.Finite (mulSupport (mulIndicator s f))
hg : Set.Finite (mulSupport (mulIndicator s g))
⊢ (∏ᶠ (i : α) (_ : i ∈ s), f i * g i) = (∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ s), g i
simp only [finprod_mem_def, mulIndicator_mul, finprod_mul_distrib hf hg]