rw [← vecMulLinear_transpose, vecMulLinear_injective_iff]
R : Type u_1
m : Type u_2
n : Type u_3
inst✝¹ : CommRing R
M : Matrix m n R
inst✝ : Fintype n
⊢ Function.Injective ⇑M.mulVecLin ↔ LinearIndependent R fun i => Mᵀ i
no goals