Theorem: Matrix.mem_colSpace_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
inst✝¹ : CommRing R
inst✝ : Fintype n
x : m → R
⊢ x ∈ A.colSpace ↔ ∃ y, x = A *ᵥ y
Tactic:
rw [← rowSpace_transpose, mem_rowSpace_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
inst✝¹ : CommRing R
inst✝ : Fintype n
x : m → R
⊢ (∃ y, x = y ᵥ* Aᵀ) ↔ ∃ y, x = A *ᵥ y

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
inst✝¹ : CommRing R
inst✝ : Fintype n
x : m → R
⊢ (∃ y, x = y ᵥ* Aᵀ) ↔ ∃ y, x = A *ᵥ y
Tactic:
simp [vecMul_transpose]
State after:
no goals