internlm/Lean-Github huggingface dataset:
Theorem: Matrix.cols_linearIndependent_iff_of_rowSpaces_eq
Proof 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
m₁ : Type u_15
m₂ : Type u_16
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
h : A₁.rowSpace = A₂.rowSpace
t : Set n
⊢ LinearIndependent (ι := ↑t) K (A₁.colSubmatrix t).colFun ↔ LinearIndependent (ι := ↑t) K (A₂.colSubmatrix t).colFun
Tactic:
exact ⟨fun h' ↦ cols_linearIndependent_of_rowSpace_le_rowSpace h.le h',
  fun h' ↦ cols_linearIndependent_of_rowSpace_le_rowSpace h.symm.le h'⟩
Proof state after:
no goals
Theorem: Matrix.colBases_eq_of_rowSpaces_eq
Proof 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
m₁ : Type u_15
m₂ : Type u_16
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
h : A₁.rowSpace = A₂.rowSpace
⊢ A₁.ColBasis = A₂.ColBasis
Tactic:
ext
Proof state after:
case h.a
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
m₁ : Type u_15
m₂ : Type u_16
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
h : A₁.rowSpace = A₂.rowSpace
x✝ : Set n
⊢ A₁.ColBasis x✝ ↔ A₂.ColBasis x✝
Theorem: Matrix.colBases_eq_of_rowSpaces_eq
Proof state before:
case h.a
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
m₁ : Type u_15
m₂ : Type u_16
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
h : A₁.rowSpace = A₂.rowSpace
x✝ : Set n
⊢ A₁.ColBasis x✝ ↔ A₂.ColBasis x✝
Tactic:
simp_rw [colBasis_iff_maximal_linearIndependent, cols_linearIndependent_iff_of_rowSpaces_eq h]
Proof state after:
no goals
Theorem: Matrix.rowsLinearIndependent_iff_of_colSpaces_eq
Proof 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
m₁ : Type u_15
m₂ : Type u_16
A₁✝ : Matrix m₁ n K
A₂✝ : Matrix m₂ n K
A₁ : Matrix m n₁ K
A₂ : Matrix m n₂ K
h : A₁.colSpace = A₂.colSpace
⊢ LinearIndependent (ι := ↑s) K (A₁.rowSubmatrix s).rowFun ↔ LinearIndependent (ι := ↑s) K (A₂.rowSubmatrix s).rowFun
Tactic:
rw [← rowSpace_transpose, ← rowSpace_transpose] at h
Proof 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
m₁ : Type u_15
m₂ : Type u_16
A₁✝ : Matrix m₁ n K
A₂✝ : Matrix m₂ n K
A₁ : Matrix m n₁ K
A₂ : Matrix m n₂ K
h : A₁ᵀ.rowSpace = A₂ᵀ.rowSpace
⊢ LinearIndependent (ι := ↑s) K (A₁.rowSubmatrix s).rowFun ↔ LinearIndependent (ι := ↑s) K (A₂.rowSubmatrix s).rowFun
Theorem: Matrix.rowsLinearIndependent_iff_of_colSpaces_eq
Proof 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
m₁ : Type u_15
m₂ : Type u_16
A₁✝ : Matrix m₁ n K
A₂✝ : Matrix m₂ n K
A₁ : Matrix m n₁ K
A₂ : Matrix m n₂ K
h : A₁ᵀ.rowSpace = A₂ᵀ.rowSpace
⊢ LinearIndependent (ι := ↑s) K (A₁.rowSubmatrix s).rowFun ↔ LinearIndependent (ι := ↑s) K (A₂.rowSubmatrix s).rowFun
Tactic:
exact cols_linearIndependent_iff_of_rowSpaces_eq h
Proof state after:
no goals
Theorem: Matrix.rowBases_eq_of_colSpaces_eq
Proof 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
m₁ : Type u_15
m₂ : Type u_16
A₁✝ : Matrix m₁ n K
A₂✝ : Matrix m₂ n K
A₁ : Matrix m n₁ K
A₂ : Matrix m n₂ K
h : A₁.colSpace = A₂.colSpace
⊢ A₁.RowBasis = A₂.RowBasis
Tactic:
ext s
Proof state after:
case h.a
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
m₁ : Type u_15
m₂ : Type u_16
A₁✝ : Matrix m₁ n K
A₂✝ : Matrix m₂ n K
A₁ : Matrix m n₁ K
A₂ : Matrix m n₂ K
h : A₁.colSpace = A₂.colSpace
s : Set m
⊢ A₁.RowBasis s ↔ A₂.RowBasis s
Theorem: Matrix.rowBases_eq_of_colSpaces_eq
Proof state before:
case h.a
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
m₁ : Type u_15
m₂ : Type u_16
A₁✝ : Matrix m₁ n K
A₂✝ : Matrix m₂ n K
A₁ : Matrix m n₁ K
A₂ : Matrix m n₂ K
h : A₁.colSpace = A₂.colSpace
s : Set m
⊢ A₁.RowBasis s ↔ A₂.RowBasis s
Tactic:
rw [← rowSpace_transpose, ← rowSpace_transpose] at h
Proof state after:
case h.a
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
m₁ : Type u_15
m₂ : Type u_16
A₁✝ : Matrix m₁ n K
A₂✝ : Matrix m₂ n K
A₁ : Matrix m n₁ K
A₂ : Matrix m n₂ K
h : A₁ᵀ.rowSpace = A₂ᵀ.rowSpace
s : Set m
⊢ A₁.RowBasis s ↔ A₂.RowBasis s
Theorem: Matrix.rowBases_eq_of_colSpaces_eq
Proof state before:
case h.a
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
m₁ : Type u_15
m₂ : Type u_16
A₁✝ : Matrix m₁ n K
A₂✝ : Matrix m₂ n K
A₁ : Matrix m n₁ K
A₂ : Matrix m n₂ K
h : A₁ᵀ.rowSpace = A₂ᵀ.rowSpace
s : Set m
⊢ A₁.RowBasis s ↔ A₂.RowBasis s
Tactic:
simpa using congr_fun (colBases_eq_of_rowSpaces_eq h) s
Proof state after:
no goals
Theorem: Matrix.RowBasis.submatrix_colBasis
Proof 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
m₁ : Type u_15
m₂ : Type u_16
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
hs : A.RowBasis s
ht : A.ColBasis t
⊢ (A.rowSubmatrix s).ColBasis t
Tactic:
rwa [colBases_eq_of_rowSpaces_eq hs.rowSpace_eq]
Proof state after:
no goals
Theorem: Matrix.ColBasis.submatrix_rowBasis
Proof 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
m₁ : Type u_15
m₂ : Type u_16
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
ht : A.ColBasis t
hs : A.RowBasis s
⊢ (A.colSubmatrix t).RowBasis s
Tactic:
rwa [rowBases_eq_of_colSpaces_eq ht.colSpace_eq]
Proof state after:
no goals
Theorem: Matrix.ColBasis.basisFun_apply
Proof 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
m₁ : Type u_15
m₂ : Type u_16
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
inst✝ : Fintype m
ht : A.ColBasis t
hA : LinearIndependent K A.rowFun
j : ↑t
⊢ (ht.basisFun hA) j = fun x => A x ↑j
Tactic:
ext x
Proof state after:
case 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
K : Type u_14
inst✝¹ : Field K
A : Matrix m n K
m₁ : Type u_15
m₂ : Type u_16
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
inst✝ : Fintype m
ht : A.ColBasis t
hA : LinearIndependent K A.rowFun
j : ↑t
x : m
⊢ (ht.basisFun hA) j x = A x ↑j
Theorem: Matrix.ColBasis.basisFun_apply
Proof state before:
case 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
K : Type u_14
inst✝¹ : Field K
A : Matrix m n K
m₁ : Type u_15
m₂ : Type u_16
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
inst✝ : Fintype m
ht : A.ColBasis t
hA : LinearIndependent K A.rowFun
j : ↑t
x : m
⊢ (ht.basisFun hA) j x = A x ↑j
Tactic:
exact congr_fun (Basis.span_apply ht.linearIndependent j) x
Proof state after:
no goals
Theorem: Matrix.RowBasis.basisFun_apply
Proof 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
m₁ : Type u_15
m₂ : Type u_16
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
inst✝ : Fintype n
hs : A.RowBasis s
hA : LinearIndependent K Aᵀ
i : ↑s
⊢ (hs.basisFun hA) i = A ↑i
Tactic:
ext
Proof state after:
case 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
K : Type u_14
inst✝¹ : Field K
A : Matrix m n K
m₁ : Type u_15
m₂ : Type u_16
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
inst✝ : Fintype n
hs : A.RowBasis s
hA : LinearIndependent K Aᵀ
i : ↑s
x✝ : n
⊢ (hs.basisFun hA) i x✝ = A (↑i) x✝
Theorem: Matrix.RowBasis.basisFun_apply
Proof state before:
case 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
K : Type u_14
inst✝¹ : Field K
A : Matrix m n K
m₁ : Type u_15
m₂ : Type u_16
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
inst✝ : Fintype n
hs : A.RowBasis s
hA : LinearIndependent K Aᵀ
i : ↑s
x✝ : n
⊢ (hs.basisFun hA) i x✝ = A (↑i) x✝
Tactic:
simp [basisFun]
Proof state after:
no goals
Theorem: Matrix.mem_nullSpace_iff
Proof 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
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
x : n → K
⊢ x ∈ A.nullSpace ↔ A *ᵥ x = 0
Tactic:
simp only [nullSpace, mem_orthSpace_iff', mulVec, dotProduct, mul_comm (x _)]
Proof 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
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
x : n → K
⊢ (∀ y ∈ A.rowSpace, ∑ x_1 : n, y x_1 * x x_1 = 0) ↔ A *ᵥ x = 0
Theorem: Matrix.mem_nullSpace_iff
Proof 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
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
x : n → K
⊢ (∀ y ∈ A.rowSpace, ∑ x_1 : n, y x_1 * x x_1 = 0) ↔ A *ᵥ x = 0
Tactic:
refine ⟨fun h ↦ funext fun i ↦ h _ (subset_span <| mem_range_self i), fun h y hy ↦ ?_⟩
Proof 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
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
x : n → K
h : A *ᵥ x = 0
y : n → K
hy : y ∈ A.rowSpace
⊢ ∑ x_1 : n, y x_1 * x x_1 = 0
Theorem: Matrix.mem_nullSpace_iff
Proof 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
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
x : n → K
h : A *ᵥ x = 0
y : n → K
hy : y ∈ A.rowSpace
⊢ ∑ x_1 : n, y x_1 * x x_1 = 0
Tactic:
rw [rowSpace] at hy
Proof 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
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
x : n → K
h : A *ᵥ x = 0
y : n → K
hy : y ∈ span K (range A.rowFun)
⊢ ∑ x_1 : n, y x_1 * x x_1 = 0
Theorem: Matrix.mem_nullSpace_iff
Proof 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
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
x : n → K
h : A *ᵥ x = 0
y : n → K
hy : y ∈ span K (range A.rowFun)
⊢ ∑ x_1 : n, y x_1 * x x_1 = 0
Tactic:
rw [← dotProduct_eq_zero_of_mem_span hy (x := x)]
Proof 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
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
x : n → K
h : A *ᵥ x = 0
y : n → K
hy : y ∈ span K (range A.rowFun)
⊢ ∑ x_1 : n, y x_1 * x x_1 = x ⬝ᵥ y

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
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
x : n → K
h : A *ᵥ x = 0
y : n → K
hy : y ∈ span K (range A.rowFun)
⊢ ∀ z ∈ range A.rowFun, x ⬝ᵥ z = 0
Theorem: Matrix.mem_nullSpace_iff
Proof 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
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
x : n → K
h : A *ᵥ x = 0
y : n → K
hy : y ∈ span K (range A.rowFun)
⊢ ∀ z ∈ range A.rowFun, x ⬝ᵥ z = 0
Tactic:
rintro _ ⟨a ,ha, rfl⟩
Proof state after:
case intro.refl
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
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
x : n → K
h : A *ᵥ x = 0
y : n → K
hy : y ∈ span K (range A.rowFun)
a : m
⊢ x ⬝ᵥ A.rowFun a = 0
Theorem: Matrix.mem_nullSpace_iff
Proof state before:
case intro.refl
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
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
x : n → K
h : A *ᵥ x = 0
y : n → K
hy : y ∈ span K (range A.rowFun)
a : m
⊢ x ⬝ᵥ A.rowFun a = 0
Tactic:
convert congr_fun h a using 1
Proof state after:
case h.e'_2
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
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
x : n → K
h : A *ᵥ x = 0
y : n → K
hy : y ∈ span K (range A.rowFun)
a : m
⊢ x ⬝ᵥ A.rowFun a = (A *ᵥ x) a
Theorem: Matrix.mem_nullSpace_iff
Proof state before:
case h.e'_2
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
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
x : n → K
h : A *ᵥ x = 0
y : n → K
hy : y ∈ span K (range A.rowFun)
a : m
⊢ x ⬝ᵥ A.rowFun a = (A *ᵥ x) a
Tactic:
simp [dotProduct, mul_comm, mulVec]
Proof state after:
no goals
Theorem: Matrix.mem_nullSpace_iff
Proof 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
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
x : n → K
h : A *ᵥ x = 0
y : n → K
hy : y ∈ span K (range A.rowFun)
⊢ ∑ x_1 : n, y x_1 * x x_1 = x ⬝ᵥ y
Tactic:
simp [dotProduct, mul_comm]
Proof state after:
no goals
Theorem: Matrix.orthSpace_nullSpace_eq_rowSpace
Proof 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
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
⊢ A.nullSpace.orthSpace = A.rowSpace
Tactic:
rw [← orthSpace_rowSpace_eq_nullSpace, orthSpace_orthSpace]
Proof state after:
no goals
Theorem: Matrix.nullSpace_eq_ker_mulVecLin
Proof 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
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
⊢ A.nullSpace = LinearMap.ker A.mulVecLin
Tactic:
ext x
Proof state after:
case 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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
x : n → K
⊢ x ∈ A.nullSpace ↔ x ∈ LinearMap.ker A.mulVecLin
Theorem: Matrix.nullSpace_eq_ker_mulVecLin
Proof state before:
case 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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
x : n → K
⊢ x ∈ A.nullSpace ↔ x ∈ LinearMap.ker A.mulVecLin
Tactic:
rw [mem_nullSpace_iff, LinearMap.mem_ker, mulVecLin_apply]
Proof state after:
no goals