Theorem: Matrix.subset_cols_notLinearIndependent_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
K : Type u_14
inst✝¹ : Field K
A : Matrix m n K
inst✝ : Fintype n
⊢ ¬LinearIndependent (ι := ↑t) K (A.colSubmatrix t).colFun ↔ ∃ c, A *ᵥ c = 0 ∧ c ≠ 0 ∧ support c ⊆ t
Tactic:
rw [← rowFun_transpose, colSubmatrix_transpose, subset_rows_notLinearIndependent_iff]
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
K : Type u_14
inst✝¹ : Field K
A : Matrix m n K
inst✝ : Fintype n
⊢ (∃ c, c ᵥ* Aᵀ = 0 ∧ c ≠ 0 ∧ support c ⊆ t) ↔ ∃ c, A *ᵥ c = 0 ∧ c ≠ 0 ∧ support c ⊆ t

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
K : Type u_14
inst✝¹ : Field K
A : Matrix m n K
inst✝ : Fintype n
⊢ (∃ c, c ᵥ* Aᵀ = 0 ∧ c ≠ 0 ∧ support c ⊆ t) ↔ ∃ c, A *ᵥ c = 0 ∧ c ≠ 0 ∧ support c ⊆ t
Tactic:
simp_rw [vecMul_transpose]
State after:
no goals