rw [← vecMul_injective_iff]
R✝ : Type u_1
m : Type u_2
n : Type u_3
inst✝² : Semiring R✝
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Fintype m
M : Matrix m n R
⊢ Function.Injective ⇑M.vecMulLinear ↔ LinearIndependent R fun i => M i
R✝ : Type u_1
m : Type u_2
n : Type u_3
inst✝² : Semiring R✝
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Fintype m
M : Matrix m n R
⊢ Function.Injective ⇑M.vecMulLinear ↔ Function.Injective fun v => v ᵥ* fun i => M i