no goals
R : Type u_2
S : Type u_1
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 x' : S
h : ↑(leftMulMatrix b) x = ↑(leftMulMatrix b) x'
⊢ ↑(↑(lmul R S) x) 1 = ↑(↑(lmul R S) x') 1
rw [(LinearMap.toMatrix b b).injective h]