no goals
ι : Type u_1
ι' : Type ?u.456903
R : Type u_2
R₂ : Type ?u.456909
K : Type ?u.456912
M : Type u_3
M' : Type ?u.456918
M'' : Type ?u.456921
V : Type u
V' : Type ?u.456926
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b b₁ : Basis ι R M
i : ι
c : R
x : M
l : ι →₀ R
hl : ↑(Finsupp.total ι M R ↑b) l = 0
⊢ ↑b.repr (↑(Finsupp.total ι M R ↑b) l) = 0
rw [hl, LinearEquiv.map_zero]