rw [submatrix_eq_restrict, linearIndependent_restrict_iff] at *
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✝
R : Type u_14
inst✝ : CommSemiring R
s s' : Set m
t t' : Set n
A : Matrix m n R
h : LinearIndependent (ι := ↑s) R (A.submatrix s.incl t.incl).rowFun
h' : LinearIndependent (ι := ↑s') R (A.submatrix s'.incl t'.incl).rowFun
h0 : A.submatrix s.incl t'.incl = 0
⊢ LinearIndependent (ι := ↑(s ∪ s')) R (A.submatrix (s ∪ s').incl (t ∪ t').incl).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✝
R : Type u_14
inst✝ : CommSemiring R
s s' : Set m
t t' : Set n
A : Matrix m n R
h : ∀ (l : m →₀ R), (Finsupp.total m (↑t → R) R (A.colSubmatrix t)) l = 0 → ↑l.support ⊆ s → l = 0
h' : ∀ (l : m →₀ R), (Finsupp.total m (↑t' → R) R (A.colSubmatrix t')) l = 0 → ↑l.support ⊆ s' → l = 0
h0 : s.restrict (A.colSubmatrix t') = 0
⊢ ∀ (l : m →₀ R), (Finsupp.total m (↑(t ∪ t') → R) R (A.colSubmatrix (t ∪ t'))) l = 0 → ↑l.support ⊆ s ∪ s' → l = 0