rw [linearIndependent_iff'] at h ⊢
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
m₀ : Type u_14
n₀ : Type u_15
e : m₀ ≃ m
f : n₀ → n
h : LinearIndependent R (A.submatrix (⇑e) f).rowFun
⊢ LinearIndependent R A.rowFun
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
m₀ : Type u_14
n₀ : Type u_15
e : m₀ ≃ m
f : n₀ → n
h : ∀ (s : Finset m₀) (g : m₀ → R), ∑ i ∈ s, g i • (A.submatrix (⇑e) f).rowFun i = 0 → ∀ i ∈ s, g i = 0
⊢ ∀ (s : Finset m) (g : m → R), ∑ i ∈ s, g i • A.rowFun i = 0 → ∀ i ∈ s, g i = 0