Theorem: Matrix.cols_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✝
R : Type u_14
inst✝¹ : CommRing R
A : Matrix m n R
inst✝ : Fintype n
⊢ LinearIndependent R A.colFun ↔ LinearMap.ker A.mulVecLin = ⊥
Tactic:
rw [← rowFun_transpose, rows_linearIndependent_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✝
inst✝² : Ring R✝
R : Type u_14
inst✝¹ : CommRing R
A : Matrix m n R
inst✝ : Fintype n
⊢ LinearMap.ker Aᵀ.vecMulLinear = ⊥ ↔ LinearMap.ker A.mulVecLin = ⊥

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✝
R : Type u_14
inst✝¹ : CommRing R
A : Matrix m n R
inst✝ : Fintype n
⊢ LinearMap.ker Aᵀ.vecMulLinear = ⊥ ↔ LinearMap.ker A.mulVecLin = ⊥
Tactic:
convert Iff.rfl
State after:
case h.e'_2.h.e'_2.h.e'_15
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✝¹ : CommRing R
A : Matrix m n R
inst✝ : Fintype n
⊢ A.mulVecLin = Aᵀ.vecMulLinear

State before:
case h.e'_2.h.e'_2.h.e'_15
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✝¹ : CommRing R
A : Matrix m n R
inst✝ : Fintype n
⊢ A.mulVecLin = Aᵀ.vecMulLinear
Tactic:
ext
State after:
case h.e'_2.h.e'_2.h.e'_15.h.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✝
R : Type u_14
inst✝¹ : CommRing R
A : Matrix m n R
inst✝ : Fintype n
x✝¹ : n → R
x✝ : m
⊢ A.mulVecLin x✝¹ x✝ = Aᵀ.vecMulLinear x✝¹ x✝

State before:
case h.e'_2.h.e'_2.h.e'_15.h.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✝
R : Type u_14
inst✝¹ : CommRing R
A : Matrix m n R
inst✝ : Fintype n
x✝¹ : n → R
x✝ : m
⊢ A.mulVecLin x✝¹ x✝ = Aᵀ.vecMulLinear x✝¹ x✝
Tactic:
simp [← mulVec_transpose]
State after:
no goals