no goals
ι : Type u_2
ι' : Type ?u.642672
R : Type u_3
R₂ : Type ?u.642678
K : Type ?u.642681
M : Type u_1
M' : Type ?u.642687
M'' : Type ?u.642690
V : Type u
V' : Type ?u.642695
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
inst✝ : Fintype ι
b : Basis ι R M
x : ι → R
⊢ ↑(LinearEquiv.symm (equivFun b)) x = ∑ i : ι, x i • ↑b i
simp [Basis.equivFun, Finsupp.total_apply, Finsupp.sum_fintype, Finsupp.equivFunOnFinite]