Theorem: Matrix.mulVecLin_injective_iff (Matroid/ForMathlib/LinearAlgebra/Matrix/ToLin.lean)

State before:
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
Tactic:
rw [← vecMulLinear_transpose, vecMulLinear_injective_iff]
State after:
no goals