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
⊢ ↑(leftMulMatrix b) x i j = ↑(↑b.repr (x * ↑b j)) i
rw [leftMulMatrix_apply, toMatrix_lmul' b x i j]