α : Type u_1
β : Type u_2
R : Type u_4
M : Type u_3
ι : Type ?u.35638
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r s✝ : R
x y : M
f : α → R
g : β → M
s : Finset α
t : Finset β
⊢ ∀ (x : α), x ∈ s → f x • ∑ i in t, g i = ∑ y in t, f (x, y).fst • g (x, y).snd
α : Type u_1
β : Type u_2
R : Type u_4
M : Type u_3
ι : Type ?u.35638
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r s✝ : R
x y : M
f : α → R
g : β → M
s : Finset α
t : Finset β
⊢ (∑ i in s, f i) • ∑ i in t, g i = ∑ p in s ×ˢ t, f p.fst • g p.snd
rw [Finset.sum_product, Finset.sum_smul, Finset.sum_congr rfl]
α : Type u_1
β : Type u_2
R : Type u_4
M : Type u_3
ι : Type ?u.35638
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r s✝ : R
x y : M
f : α → R
g : β → M
s : Finset α
t : Finset β
x✝ : α
a✝ : x✝ ∈ s
⊢ f x✝ • ∑ i in t, g i = ∑ y in t, f (x✝, y).fst • g (x✝, y).snd
α : Type u_1
β : Type u_2
R : Type u_4
M : Type u_3
ι : Type ?u.35638
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r s✝ : R
x y : M
f : α → R
g : β → M
s : Finset α
t : Finset β
⊢ ∀ (x : α), x ∈ s → f x • ∑ i in t, g i = ∑ y in t, f (x, y).fst • g (x, y).snd
intros
no goals
α : Type u_1
β : Type u_2
R : Type u_4
M : Type u_3
ι : Type ?u.35638
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r s✝ : R
x y : M
f : α → R
g : β → M
s : Finset α
t : Finset β
x✝ : α
a✝ : x✝ ∈ s
⊢ f x✝ • ∑ i in t, g i = ∑ y in t, f (x✝, y).fst • g (x✝, y).snd
rw [Finset.smul_sum]