internlm/Lean-Github huggingface dataset:
Theorem: Matroid.freeOn_er_eq
Proof state before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
E : Set α
hXE : X ⊆ E
⊢ (freeOn E).er X = X.encard
Tactic:
obtain ⟨I, hI⟩ := (freeOn E).exists_basis X
Proof state after:
case intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I✝ B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
E : Set α
hXE : X ⊆ E
I : Set α
hI : (freeOn E).Basis I X
⊢ (freeOn E).er X = X.encard
Theorem: Matroid.freeOn_er_eq
Proof state before:
case intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I✝ B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
E : Set α
hXE : X ⊆ E
I : Set α
hI : (freeOn E).Basis I X
⊢ (freeOn E).er X = X.encard
Tactic:
rw [hI.er_eq_encard, (freeOn_indep hXE).eq_of_basis hI]
Proof state after:
no goals
Theorem: Matroid.freeOn_r_eq
Proof state before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
E : Set α
hXE : X ⊆ E
⊢ (freeOn E).r X = X.ncard
Tactic:
rw [← er_toNat_eq_r, freeOn_er_eq hXE, ncard_def]
Proof state after:
no goals
Theorem: Matrix.mem_rowSpace_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
inst✝¹ : CommRing R
inst✝ : Fintype m
x : n → R
⊢ x ∈ A.rowSpace ↔ ∃ y, x = y ᵥ* A
Tactic:
simp [rowSpace_eq_lin_range, eq_comm]
Proof state after:
no goals
Theorem: Matrix.mem_colSpace_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
inst✝¹ : CommRing R
inst✝ : Fintype n
x : m → R
⊢ x ∈ A.colSpace ↔ ∃ y, x = A *ᵥ y
Tactic:
rw [← rowSpace_transpose, mem_rowSpace_iff]
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
inst✝¹ : CommRing R
inst✝ : Fintype n
x : m → R
⊢ (∃ y, x = y ᵥ* Aᵀ) ↔ ∃ y, x = A *ᵥ y
Theorem: Matrix.mem_colSpace_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
inst✝¹ : CommRing R
inst✝ : Fintype n
x : m → R
⊢ (∃ y, x = y ᵥ* Aᵀ) ↔ ∃ y, x = A *ᵥ y
Tactic:
simp [vecMul_transpose]
Proof state after:
no goals
Theorem: Matrix.vecMul_mem_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
inst✝¹ : CommRing R
inst✝ : Fintype m
A : Matrix m n R
c : m → R
⊢ c ᵥ* A ∈ A.rowSpace
Tactic:
rw [mem_rowSpace_iff]
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
inst✝¹ : CommRing R
inst✝ : Fintype m
A : Matrix m n R
c : m → R
⊢ ∃ y, c ᵥ* A = y ᵥ* A
Theorem: Matrix.vecMul_mem_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
inst✝¹ : CommRing R
inst✝ : Fintype m
A : Matrix m n R
c : m → R
⊢ ∃ y, c ᵥ* A = y ᵥ* A
Tactic:
exact ⟨_, rfl⟩
Proof state after:
no goals
Theorem: Matrix.mulVec_mem_colSpace
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
inst✝¹ : CommRing R
inst✝ : Fintype n
A : Matrix m n R
c : n → R
⊢ A *ᵥ c ∈ A.colSpace
Tactic:
rw [mem_colSpace_iff]
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
inst✝¹ : CommRing R
inst✝ : Fintype n
A : Matrix m n R
c : n → R
⊢ ∃ y, A *ᵥ c = A *ᵥ y
Theorem: Matrix.mulVec_mem_colSpace
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
inst✝¹ : CommRing R
inst✝ : Fintype n
A : Matrix m n R
c : n → R
⊢ ∃ y, A *ᵥ c = A *ᵥ y
Tactic:
exact ⟨_, rfl⟩
Proof state after:
no goals
Theorem: Matrix.image_eq_range_submatrix
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
A : Matrix m n α
s : Set m
⊢ A '' s = range (A.rowSubmatrix s).rowFun
Tactic:
aesop
Proof state after:
no goals
Theorem: Matrix.dotProduct_eq_zero_of_mem_span
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
inst✝¹ : Fintype m
inst✝ : CommSemiring R
x y : m → R
s : Set (m → R)
hy : y ∈ span R s
h : ∀ z ∈ s, x ⬝ᵥ z = 0
⊢ x ⬝ᵥ y = 0
Tactic:
obtain ⟨c, y,z, rfl⟩ := mem_span_set'.1 hy
Proof state after:
case intro.intro.intro
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✝¹ : Fintype m
inst✝ : CommSemiring R
x : m → R
s : Set (m → R)
h : ∀ z ∈ s, x ⬝ᵥ z = 0
c : ℕ
y : Fin c → R
z : Fin c → ↑s
hy : ∑ i : Fin c, y i • ↑(z i) ∈ span R s
⊢ x ⬝ᵥ ∑ i : Fin c, y i • ↑(z i) = 0
Theorem: Matrix.dotProduct_eq_zero_of_mem_span
Proof state before:
case intro.intro.intro
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✝¹ : Fintype m
inst✝ : CommSemiring R
x : m → R
s : Set (m → R)
h : ∀ z ∈ s, x ⬝ᵥ z = 0
c : ℕ
y : Fin c → R
z : Fin c → ↑s
hy : ∑ i : Fin c, y i • ↑(z i) ∈ span R s
⊢ x ⬝ᵥ ∑ i : Fin c, y i • ↑(z i) = 0
Tactic:
simp only [dotProduct, Finset.sum_apply, Pi.smul_apply, smul_eq_mul, Finset.mul_sum]
Proof state after:
case intro.intro.intro
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✝¹ : Fintype m
inst✝ : CommSemiring R
x : m → R
s : Set (m → R)
h : ∀ z ∈ s, x ⬝ᵥ z = 0
c : ℕ
y : Fin c → R
z : Fin c → ↑s
hy : ∑ i : Fin c, y i • ↑(z i) ∈ span R s
⊢ ∑ x_1 : m, ∑ i : Fin c, x x_1 * (y i * ↑(z i) x_1) = 0
Theorem: Matrix.dotProduct_eq_zero_of_mem_span
Proof state before:
case intro.intro.intro
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✝¹ : Fintype m
inst✝ : CommSemiring R
x : m → R
s : Set (m → R)
h : ∀ z ∈ s, x ⬝ᵥ z = 0
c : ℕ
y : Fin c → R
z : Fin c → ↑s
hy : ∑ i : Fin c, y i • ↑(z i) ∈ span R s
⊢ ∑ x_1 : m, ∑ i : Fin c, x x_1 * (y i * ↑(z i) x_1) = 0
Tactic:
rw [Finset.sum_comm, Finset.sum_eq_zero]
Proof state after:
case intro.intro.intro
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✝¹ : Fintype m
inst✝ : CommSemiring R
x : m → R
s : Set (m → R)
h : ∀ z ∈ s, x ⬝ᵥ z = 0
c : ℕ
y : Fin c → R
z : Fin c → ↑s
hy : ∑ i : Fin c, y i • ↑(z i) ∈ span R s
⊢ ∀ x_1 ∈ Finset.univ, ∑ x_2 : m, x x_2 * (y x_1 * ↑(z x_1) x_2) = 0
Theorem: Matrix.dotProduct_eq_zero_of_mem_span
Proof state before:
case intro.intro.intro
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✝¹ : Fintype m
inst✝ : CommSemiring R
x : m → R
s : Set (m → R)
h : ∀ z ∈ s, x ⬝ᵥ z = 0
c : ℕ
y : Fin c → R
z : Fin c → ↑s
hy : ∑ i : Fin c, y i • ↑(z i) ∈ span R s
⊢ ∀ x_1 ∈ Finset.univ, ∑ x_2 : m, x x_2 * (y x_1 * ↑(z x_1) x_2) = 0
Tactic:
rintro w -
Proof state after:
case intro.intro.intro
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✝¹ : Fintype m
inst✝ : CommSemiring R
x : m → R
s : Set (m → R)
h : ∀ z ∈ s, x ⬝ᵥ z = 0
c : ℕ
y : Fin c → R
z : Fin c → ↑s
hy : ∑ i : Fin c, y i • ↑(z i) ∈ span R s
w : Fin c
⊢ ∑ x_1 : m, x x_1 * (y w * ↑(z w) x_1) = 0
Theorem: Matrix.dotProduct_eq_zero_of_mem_span
Proof state before:
case intro.intro.intro
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✝¹ : Fintype m
inst✝ : CommSemiring R
x : m → R
s : Set (m → R)
h : ∀ z ∈ s, x ⬝ᵥ z = 0
c : ℕ
y : Fin c → R
z : Fin c → ↑s
hy : ∑ i : Fin c, y i • ↑(z i) ∈ span R s
w : Fin c
⊢ ∑ x_1 : m, x x_1 * (y w * ↑(z w) x_1) = 0
Tactic:
obtain ⟨i, hi⟩ := z w
Proof state after:
case intro.intro.intro.mk
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✝¹ : Fintype m
inst✝ : CommSemiring R
x : m → R
s : Set (m → R)
h : ∀ z ∈ s, x ⬝ᵥ z = 0
c : ℕ
y : Fin c → R
z : Fin c → ↑s
hy : ∑ i : Fin c, y i • ↑(z i) ∈ span R s
w : Fin c
i : m → R
hi : i ∈ s
⊢ ∑ x_1 : m, x x_1 * (y w * ↑⟨i, hi⟩ x_1) = 0
Theorem: Matrix.dotProduct_eq_zero_of_mem_span
Proof state before:
case intro.intro.intro.mk
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✝¹ : Fintype m
inst✝ : CommSemiring R
x : m → R
s : Set (m → R)
h : ∀ z ∈ s, x ⬝ᵥ z = 0
c : ℕ
y : Fin c → R
z : Fin c → ↑s
hy : ∑ i : Fin c, y i • ↑(z i) ∈ span R s
w : Fin c
i : m → R
hi : i ∈ s
⊢ ∑ x_1 : m, x x_1 * (y w * ↑⟨i, hi⟩ x_1) = 0
Tactic:
simp_rw [mul_comm (y w), ← mul_assoc, ← Finset.sum_mul]
Proof state after:
case intro.intro.intro.mk
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✝¹ : Fintype m
inst✝ : CommSemiring R
x : m → R
s : Set (m → R)
h : ∀ z ∈ s, x ⬝ᵥ z = 0
c : ℕ
y : Fin c → R
z : Fin c → ↑s
hy : ∑ i : Fin c, y i • ↑(z i) ∈ span R s
w : Fin c
i : m → R
hi : i ∈ s
⊢ (∑ i_1 : m, x i_1 * i i_1) * y w = 0
Theorem: Matrix.dotProduct_eq_zero_of_mem_span
Proof state before:
case intro.intro.intro.mk
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✝¹ : Fintype m
inst✝ : CommSemiring R
x : m → R
s : Set (m → R)
h : ∀ z ∈ s, x ⬝ᵥ z = 0
c : ℕ
y : Fin c → R
z : Fin c → ↑s
hy : ∑ i : Fin c, y i • ↑(z i) ∈ span R s
w : Fin c
i : m → R
hi : i ∈ s
⊢ (∑ i_1 : m, x i_1 * i i_1) * y w = 0
Tactic:
convert zero_mul _
Proof state after:
case h.e'_2.h.e'_5
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✝¹ : Fintype m
inst✝ : CommSemiring R
x : m → R
s : Set (m → R)
h : ∀ z ∈ s, x ⬝ᵥ z = 0
c : ℕ
y : Fin c → R
z : Fin c → ↑s
hy : ∑ i : Fin c, y i • ↑(z i) ∈ span R s
w : Fin c
i : m → R
hi : i ∈ s
⊢ ∑ i_1 : m, x i_1 * i i_1 = 0
Theorem: Matrix.dotProduct_eq_zero_of_mem_span
Proof state before:
case h.e'_2.h.e'_5
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✝¹ : Fintype m
inst✝ : CommSemiring R
x : m → R
s : Set (m → R)
h : ∀ z ∈ s, x ⬝ᵥ z = 0
c : ℕ
y : Fin c → R
z : Fin c → ↑s
hy : ∑ i : Fin c, y i • ↑(z i) ∈ span R s
w : Fin c
i : m → R
hi : i ∈ s
⊢ ∑ i_1 : m, x i_1 * i i_1 = 0
Tactic:
rw [← h i hi, dotProduct]
Proof state after:
no goals
Theorem: Matrix.RowBasis.basis_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
inst✝ : Ring R
h : A.RowBasis s
i : ↑s
⊢ ↑(h.basis 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
inst✝ : Ring R
h : A.RowBasis s
i : ↑s
x✝ : n
⊢ ↑(h.basis i) x✝ = A (↑i) x✝
Theorem: Matrix.RowBasis.basis_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
inst✝ : Ring R
h : A.RowBasis s
i : ↑s
x✝ : n
⊢ ↑(h.basis i) x✝ = A (↑i) x✝
Tactic:
simp only [basis, Basis.map_apply, LinearEquiv.coe_ofEq_apply, Basis.span_apply]
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
inst✝ : Ring R
h : A.RowBasis s
i : ↑s
x✝ : n
⊢ (A.rowSubmatrix s).rowFun i x✝ = A (↑i) x✝
Theorem: Matrix.RowBasis.basis_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
inst✝ : Ring R
h : A.RowBasis s
i : ↑s
x✝ : n
⊢ (A.rowSubmatrix s).rowFun i x✝ = A (↑i) x✝
Tactic:
rfl
Proof state after:
no goals
Theorem: Matrix.rows_linearIndependent_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
inst✝¹ : Ring R
inst✝ : Fintype m
⊢ LinearIndependent R A.rowFun ↔ LinearMap.ker A.vecMulLinear = ⊥
Tactic:
simp only [Fintype.linearIndependent_iff, Submodule.eq_bot_iff, LinearMap.mem_ker,
  vecMulLinear_apply, vecMul_eq_sum]
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
inst✝¹ : Ring R
inst✝ : Fintype m
⊢ (∀ (g : m → R), ∑ i : m, g i • A.rowFun i = 0 → ∀ (i : m), g i = 0) ↔ ∀ (x : m → R), ∑ i : m, x i • A i = 0 → x = 0
Theorem: Matrix.rows_linearIndependent_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
inst✝¹ : Ring R
inst✝ : Fintype m
⊢ (∀ (g : m → R), ∑ i : m, g i • A.rowFun i = 0 → ∀ (i : m), g i = 0) ↔ ∀ (x : m → R), ∑ i : m, x i • A i = 0 → x = 0
Tactic:
aesop
Proof state after:
no goals
Theorem: Matrix.cols_linearIndependent_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✝
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]
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✝
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 = ⊥
Theorem: Matrix.cols_linearIndependent_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✝
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
Proof 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
Theorem: Matrix.cols_linearIndependent_iff
Proof 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
Proof 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✝
Theorem: Matrix.cols_linearIndependent_iff
Proof 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]
Proof state after:
no goals
Theorem: Matrix.rows_linearIndependent_of_submatrix
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
inst✝ : Ring R
m₀ : Type u_14
n₀ : Type u_15
e : m₀ ≃ m
f : n₀ → n
h : LinearIndependent R (A.submatrix (⇑e) f).rowFun
⊢ LinearIndependent R A.rowFun
Tactic:
rw [linearIndependent_iff'] 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
inst✝ : Ring R
m₀ : Type u_14
n₀ : Type u_15
e : m₀ ≃ m
f : n₀ → n
h : ∀ (s : Finset m₀) (g : m₀ → R), ∑ i ∈ s, g i • (A.submatrix (⇑e) f).rowFun i = 0 → ∀ i ∈ s, g i = 0
⊢ ∀ (s : Finset m) (g : m → R), ∑ i ∈ s, g i • A.rowFun i = 0 → ∀ i ∈ s, g i = 0
Theorem: Matrix.rows_linearIndependent_of_submatrix
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
inst✝ : Ring R
m₀ : Type u_14
n₀ : Type u_15
e : m₀ ≃ m
f : n₀ → n
h : ∀ (s : Finset m₀) (g : m₀ → R), ∑ i ∈ s, g i • (A.submatrix (⇑e) f).rowFun i = 0 → ∀ i ∈ s, g i = 0
⊢ ∀ (s : Finset m) (g : m → R), ∑ i ∈ s, g i • A.rowFun i = 0 → ∀ i ∈ s, g i = 0
Tactic:
intro s c hc i his
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
inst✝ : Ring R
m₀ : Type u_14
n₀ : Type u_15
e : m₀ ≃ m
f : n₀ → n
h : ∀ (s : Finset m₀) (g : m₀ → R), ∑ i ∈ s, g i • (A.submatrix (⇑e) f).rowFun i = 0 → ∀ i ∈ s, g i = 0
s : Finset m
c : m → R
hc : ∑ i ∈ s, c i • A.rowFun i = 0
i : m
his : i ∈ s
⊢ c i = 0
Theorem: Matrix.rows_linearIndependent_of_submatrix
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
inst✝ : Ring R
m₀ : Type u_14
n₀ : Type u_15
e : m₀ ≃ m
f : n₀ → n
h : ∀ (s : Finset m₀) (g : m₀ → R), ∑ i ∈ s, g i • (A.submatrix (⇑e) f).rowFun i = 0 → ∀ i ∈ s, g i = 0
s : Finset m
c : m → R
hc : ∑ i ∈ s, c i • A.rowFun i = 0
i : m
his : i ∈ s
⊢ c i = 0
Tactic:
rw [← h (s.image e.symm) (c ∘ e) _ (e.symm i) (by simpa)]
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
inst✝ : Ring R
m₀ : Type u_14
n₀ : Type u_15
e : m₀ ≃ m
f : n₀ → n
h : ∀ (s : Finset m₀) (g : m₀ → R), ∑ i ∈ s, g i • (A.submatrix (⇑e) f).rowFun i = 0 → ∀ i ∈ s, g i = 0
s : Finset m
c : m → R
hc : ∑ i ∈ s, c i • A.rowFun i = 0
i : m
his : i ∈ s
⊢ c i = (c ∘ ⇑e) (e.symm i)

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
m₀ : Type u_14
n₀ : Type u_15
e : m₀ ≃ m
f : n₀ → n
h : ∀ (s : Finset m₀) (g : m₀ → R), ∑ i ∈ s, g i • (A.submatrix (⇑e) f).rowFun i = 0 → ∀ i ∈ s, g i = 0
s : Finset m
c : m → R
hc : ∑ i ∈ s, c i • A.rowFun i = 0
i : m
his : i ∈ s
⊢ ∑ i ∈ Finset.image (⇑e.symm) s, (c ∘ ⇑e) i • (A.submatrix (⇑e) f).rowFun i = 0