no goals
ι : Type u'
ι' : Type ?u.13258
R : Type u_1
K : Type ?u.13264
M : Type u_2
M' : Type ?u.13270
M'' : Type ?u.13273
V : Type u
V' : Type ?u.13278
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hf : ∀ (l : ι →₀ R), ↑(Finsupp.total ι M R v) l = 0 → l = 0
s : Finset ι
g : ι → R
hg : ∑ i in s, g i • v i = 0
i : ι
his : i ∈ s
⊢ ↑(Finsupp.total ι M R v) (∑ i in s, Finsupp.single i (g i)) = 0
simpa only [LinearMap.map_sum, Finsupp.total_single] using hg
no goals
ι : Type u'
ι' : Type ?u.13258
R : Type u_1
K : Type ?u.13264
M : Type u_2
M' : Type ?u.13270
M'' : Type ?u.13273
V : Type u
V' : Type ?u.13278
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hf : ∀ (l : ι →₀ R), ↑(Finsupp.total ι M R v) l = 0 → l = 0
s : Finset ι
g : ι → R
hg : ∑ i in s, g i • v i = 0
i : ι
his : i ∈ s
h : ∑ i in s, Finsupp.single i (g i) = 0
j : ι
_hjs : j ∈ s
hji : j ≠ i
⊢ ↑(Finsupp.lapply i) (Finsupp.single j (g j)) = 0
rw [Finsupp.lapply_apply, Finsupp.single_eq_of_ne hji]