no goals
ι : Type u_3
ι' : Type ?u.172267
R : Type u_1
R₂ : Type ?u.172273
K : Type ?u.172276
M : Type u_2
M' : Type ?u.172282
M'' : Type ?u.172285
V : Type u
V' : Type ?u.172290
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
i : ι
m : M
r : R
⊢ ↑(coord b i) (r • m) = r * ↑(coord b i) m
simp