no goals
ι : Type u_2
ι' : Type ?u.21163
R : Type u_3
R₂ : Type ?u.21169
K : Type ?u.21172
M : Type u_1
M' : Type ?u.21178
M'' : Type ?u.21181
V : Type u
V' : Type ?u.21186
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
⊢ ↑(LinearEquiv.symm b.repr) (c • Finsupp.single i 1) = c • ↑b i
rw [LinearEquiv.map_smul, repr_symm_single_one]