no goals
k : Type u_3
inst✝⁴ : CommRing k
R : Type u_1
inst✝³ : Ring R
inst✝² : Algebra k R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module k M
ι : Type u_4
b : Basis ι k M
r : R
i : ι
⊢ r • ↑(basis R b) i = r ⊗ₜ[k] ↑b i
simpa using basis_repr_symm_apply b r i