no goals
ι : Type u'
ι' : Type ?u.106583
R : Type u_1
K : Type ?u.106589
M : Type u_2
M' : Type u_3
M'' : Type ?u.106598
V : Type u
V' : Type ?u.106603
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
f : M →ₗ[R] M'
hfv : LinearIndependent R (↑f ∘ v)
s : Finset ι
g : ι → R
hg : ∑ i in s, g i • v i = 0
i : ι
his : i ∈ s
⊢ ∑ i in s, g i • ↑f (v i) = 0
simp_rw [← f.map_smul, ← f.map_sum, hg, f.map_zero]