Theorem: Matrix.rows_linearIndependent_iff (Matroid/ForMathlib/LinearAlgebra/Matrix/Rowspace.lean)

State before:
l : Type u_1
m✝ : Type u_2
m' : Type u_3
n✝ : Type u_4
n' : Type u_5
n₁ : Type u_6
n₂ : Type u_7
o : Type u_8
α : Type u_9
R✝ : Type u_10
A✝ B✝ : Matrix m✝ n✝ R✝
s✝ : Set m✝
t✝ : Set n✝
m : Type u_11
n : Type u_12
R : Type u_13
s : Set m
t : Set n
A B : Matrix m n R
inst✝¹ : Ring R
inst✝ : Fintype m
⊢ LinearIndependent R A.rowFun ↔ LinearMap.ker A.vecMulLinear = ⊥
Tactic:
simp only [Fintype.linearIndependent_iff, Submodule.eq_bot_iff, LinearMap.mem_ker,
  vecMulLinear_apply, vecMul_eq_sum]
State after:
l : Type u_1
m✝ : Type u_2
m' : Type u_3
n✝ : Type u_4
n' : Type u_5
n₁ : Type u_6
n₂ : Type u_7
o : Type u_8
α : Type u_9
R✝ : Type u_10
A✝ B✝ : Matrix m✝ n✝ R✝
s✝ : Set m✝
t✝ : Set n✝
m : Type u_11
n : Type u_12
R : Type u_13
s : Set m
t : Set n
A B : Matrix m n R
inst✝¹ : Ring R
inst✝ : Fintype m
⊢ (∀ (g : m → R), ∑ i : m, g i • A.rowFun i = 0 → ∀ (i : m), g i = 0) ↔ ∀ (x : m → R), ∑ i : m, x i • A i = 0 → x = 0

State before:
l : Type u_1
m✝ : Type u_2
m' : Type u_3
n✝ : Type u_4
n' : Type u_5
n₁ : Type u_6
n₂ : Type u_7
o : Type u_8
α : Type u_9
R✝ : Type u_10
A✝ B✝ : Matrix m✝ n✝ R✝
s✝ : Set m✝
t✝ : Set n✝
m : Type u_11
n : Type u_12
R : Type u_13
s : Set m
t : Set n
A B : Matrix m n R
inst✝¹ : Ring R
inst✝ : Fintype m
⊢ (∀ (g : m → R), ∑ i : m, g i • A.rowFun i = 0 → ∀ (i : m), g i = 0) ↔ ∀ (x : m → R), ∑ i : m, x i • A i = 0 → x = 0
Tactic:
aesop
State after:
no goals