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

State before:
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
Tactic:
rw [← vecMul_injective_iff]
State after:
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

State before:
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
Tactic:
rfl
State after:
no goals