no goals
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
m : Type u_3
inst✝¹ : Fintype m
inst✝ : DecidableEq m
b : Basis m R S
x : S
i j : m
⊢ ↑(toMatrix b b) (↑(lmul R S) x) i j = ↑(↑b.repr (x * ↑b j)) i
simp only [LinearMap.toMatrix_apply', coe_lmul_eq_mul, LinearMap.mul_apply']