internlm/Lean-Github huggingface dataset:
Theorem: MatrixCookbook.eq_399
Proof state before:
R : Type u_2
l : Type ?u.19120
m : Type u_1
n : Type u_3
p : Type ?u.19129
q : Type ?u.19132
r : Type ?u.19135
inst✝¹⁴ : Fintype l
inst✝¹³ : Fintype m
inst✝¹² : Fintype n
inst✝¹¹ : Fintype p
inst✝¹⁰ : Fintype q
inst✝⁹ : Fintype r
inst✝⁸ : DecidableEq l
inst✝⁷ : DecidableEq m
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq r
inst✝² : Field R
A₁₁ : Matrix m m R
A₁₂ : Matrix m n R
A₂₁ : Matrix n m R
A₂₂ : Matrix n n R
inst✝¹ : Invertible A₂₂
inst✝ : Invertible (A₁₁ - A₁₂ * ⅟A₂₂ * A₂₁)
this : Invertible (A₁₁.fromBlocks A₁₂ A₂₁ A₂₂) := A₁₁.fromBlocks₂₂Invertible A₁₂ A₂₁ A₂₂
⊢ (A₁₁.fromBlocks A₁₂ A₂₁ A₂₂)⁻¹ =
    let C₁ := A₁₁ - A₁₂ * ⅟A₂₂ * A₂₁;
    let i := inst✝;
    (⅟C₁).fromBlocks (-(⅟C₁ * A₁₂ * ⅟A₂₂)) (-(⅟A₂₂ * A₂₁ * ⅟C₁)) (⅟A₂₂ + ⅟A₂₂ * A₂₁ * ⅟C₁ * A₁₂ * ⅟A₂₂)
Tactic:
convert invOf_fromBlocks₂₂_eq A₁₁ A₁₂ A₂₁ A₂₂
Proof state after:
case h.e'_2
R : Type u_2
l : Type ?u.19120
m : Type u_1
n : Type u_3
p : Type ?u.19129
q : Type ?u.19132
r : Type ?u.19135
inst✝¹⁴ : Fintype l
inst✝¹³ : Fintype m
inst✝¹² : Fintype n
inst✝¹¹ : Fintype p
inst✝¹⁰ : Fintype q
inst✝⁹ : Fintype r
inst✝⁸ : DecidableEq l
inst✝⁷ : DecidableEq m
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq r
inst✝² : Field R
A₁₁ : Matrix m m R
A₁₂ : Matrix m n R
A₂₁ : Matrix n m R
A₂₂ : Matrix n n R
inst✝¹ : Invertible A₂₂
inst✝ : Invertible (A₁₁ - A₁₂ * ⅟A₂₂ * A₂₁)
this : Invertible (A₁₁.fromBlocks A₁₂ A₂₁ A₂₂) := A₁₁.fromBlocks₂₂Invertible A₁₂ A₂₁ A₂₂
⊢ (A₁₁.fromBlocks A₁₂ A₂₁ A₂₂)⁻¹ = ⅟(A₁₁.fromBlocks A₁₂ A₂₁ A₂₂)
Theorem: MatrixCookbook.eq_399
Proof state before:
case h.e'_2
R : Type u_2
l : Type ?u.19120
m : Type u_1
n : Type u_3
p : Type ?u.19129
q : Type ?u.19132
r : Type ?u.19135
inst✝¹⁴ : Fintype l
inst✝¹³ : Fintype m
inst✝¹² : Fintype n
inst✝¹¹ : Fintype p
inst✝¹⁰ : Fintype q
inst✝⁹ : Fintype r
inst✝⁸ : DecidableEq l
inst✝⁷ : DecidableEq m
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq r
inst✝² : Field R
A₁₁ : Matrix m m R
A₁₂ : Matrix m n R
A₂₁ : Matrix n m R
A₂₂ : Matrix n n R
inst✝¹ : Invertible A₂₂
inst✝ : Invertible (A₁₁ - A₁₂ * ⅟A₂₂ * A₂₁)
this : Invertible (A₁₁.fromBlocks A₁₂ A₂₁ A₂₂) := A₁₁.fromBlocks₂₂Invertible A₁₂ A₂₁ A₂₂
⊢ (A₁₁.fromBlocks A₁₂ A₂₁ A₂₂)⁻¹ = ⅟(A₁₁.fromBlocks A₁₂ A₂₁ A₂₂)
Tactic:
rw [invOf_eq_nonsing_inv]
Proof state after:
no goals
Theorem: MatrixCookbook.eq_400
Proof state before:
R : Type u_2
l : Type ?u.51145
m : Type u_1
n : Type u_3
p : Type ?u.51154
q : Type ?u.51157
r : Type ?u.51160
inst✝¹⁴ : Fintype l
inst✝¹³ : Fintype m
inst✝¹² : Fintype n
inst✝¹¹ : Fintype p
inst✝¹⁰ : Fintype q
inst✝⁹ : Fintype r
inst✝⁸ : DecidableEq l
inst✝⁷ : DecidableEq m
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq r
inst✝² : Field R
A₁₁ : Matrix m m R
A₁₂ : Matrix m n R
A₂₁ : Matrix n m R
A₂₂ : Matrix n n R
inst✝¹ : Invertible A₁₁
inst✝ : Invertible (A₂₂ - A₂₁ * ⅟A₁₁ * A₁₂)
⊢ (A₁₁.fromBlocks A₁₂ A₂₁ A₂₂)⁻¹ =
    let C₂ := A₂₂ - A₂₁ * ⅟A₁₁ * A₁₂;
    let i := inst✝;
    (⅟A₁₁ + ⅟A₁₁ * A₁₂ * ⅟C₂ * A₂₁ * ⅟A₁₁).fromBlocks (-(⅟A₁₁ * A₁₂ * ⅟C₂)) (-(⅟C₂ * A₂₁ * ⅟A₁₁)) ⅟C₂
Tactic:
letI := fromBlocks₁₁Invertible A₁₁ A₁₂ A₂₁ A₂₂
Proof state after:
R : Type u_2
l : Type ?u.51145
m : Type u_1
n : Type u_3
p : Type ?u.51154
q : Type ?u.51157
r : Type ?u.51160
inst✝¹⁴ : Fintype l
inst✝¹³ : Fintype m
inst✝¹² : Fintype n
inst✝¹¹ : Fintype p
inst✝¹⁰ : Fintype q
inst✝⁹ : Fintype r
inst✝⁸ : DecidableEq l
inst✝⁷ : DecidableEq m
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq r
inst✝² : Field R
A₁₁ : Matrix m m R
A₁₂ : Matrix m n R
A₂₁ : Matrix n m R
A₂₂ : Matrix n n R
inst✝¹ : Invertible A₁₁
inst✝ : Invertible (A₂₂ - A₂₁ * ⅟A₁₁ * A₁₂)
this : Invertible (A₁₁.fromBlocks A₁₂ A₂₁ A₂₂) := A₁₁.fromBlocks₁₁Invertible A₁₂ A₂₁ A₂₂
⊢ (A₁₁.fromBlocks A₁₂ A₂₁ A₂₂)⁻¹ =
    let C₂ := A₂₂ - A₂₁ * ⅟A₁₁ * A₁₂;
    let i := inst✝;
    (⅟A₁₁ + ⅟A₁₁ * A₁₂ * ⅟C₂ * A₂₁ * ⅟A₁₁).fromBlocks (-(⅟A₁₁ * A₁₂ * ⅟C₂)) (-(⅟C₂ * A₂₁ * ⅟A₁₁)) ⅟C₂
Theorem: MatrixCookbook.eq_400
Proof state before:
R : Type u_2
l : Type ?u.51145
m : Type u_1
n : Type u_3
p : Type ?u.51154
q : Type ?u.51157
r : Type ?u.51160
inst✝¹⁴ : Fintype l
inst✝¹³ : Fintype m
inst✝¹² : Fintype n
inst✝¹¹ : Fintype p
inst✝¹⁰ : Fintype q
inst✝⁹ : Fintype r
inst✝⁸ : DecidableEq l
inst✝⁷ : DecidableEq m
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq r
inst✝² : Field R
A₁₁ : Matrix m m R
A₁₂ : Matrix m n R
A₂₁ : Matrix n m R
A₂₂ : Matrix n n R
inst✝¹ : Invertible A₁₁
inst✝ : Invertible (A₂₂ - A₂₁ * ⅟A₁₁ * A₁₂)
this : Invertible (A₁₁.fromBlocks A₁₂ A₂₁ A₂₂) := A₁₁.fromBlocks₁₁Invertible A₁₂ A₂₁ A₂₂
⊢ (A₁₁.fromBlocks A₁₂ A₂₁ A₂₂)⁻¹ =
    let C₂ := A₂₂ - A₂₁ * ⅟A₁₁ * A₁₂;
    let i := inst✝;
    (⅟A₁₁ + ⅟A₁₁ * A₁₂ * ⅟C₂ * A₂₁ * ⅟A₁₁).fromBlocks (-(⅟A₁₁ * A₁₂ * ⅟C₂)) (-(⅟C₂ * A₂₁ * ⅟A₁₁)) ⅟C₂
Tactic:
convert invOf_fromBlocks₁₁_eq A₁₁ A₁₂ A₂₁ A₂₂
Proof state after:
case h.e'_2
R : Type u_2
l : Type ?u.51145
m : Type u_1
n : Type u_3
p : Type ?u.51154
q : Type ?u.51157
r : Type ?u.51160
inst✝¹⁴ : Fintype l
inst✝¹³ : Fintype m
inst✝¹² : Fintype n
inst✝¹¹ : Fintype p
inst✝¹⁰ : Fintype q
inst✝⁹ : Fintype r
inst✝⁸ : DecidableEq l
inst✝⁷ : DecidableEq m
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq r
inst✝² : Field R
A₁₁ : Matrix m m R
A₁₂ : Matrix m n R
A₂₁ : Matrix n m R
A₂₂ : Matrix n n R
inst✝¹ : Invertible A₁₁
inst✝ : Invertible (A₂₂ - A₂₁ * ⅟A₁₁ * A₁₂)
this : Invertible (A₁₁.fromBlocks A₁₂ A₂₁ A₂₂) := A₁₁.fromBlocks₁₁Invertible A₁₂ A₂₁ A₂₂
⊢ (A₁₁.fromBlocks A₁₂ A₂₁ A₂₂)⁻¹ = ⅟(A₁₁.fromBlocks A₁₂ A₂₁ A₂₂)
Theorem: MatrixCookbook.eq_400
Proof state before:
case h.e'_2
R : Type u_2
l : Type ?u.51145
m : Type u_1
n : Type u_3
p : Type ?u.51154
q : Type ?u.51157
r : Type ?u.51160
inst✝¹⁴ : Fintype l
inst✝¹³ : Fintype m
inst✝¹² : Fintype n
inst✝¹¹ : Fintype p
inst✝¹⁰ : Fintype q
inst✝⁹ : Fintype r
inst✝⁸ : DecidableEq l
inst✝⁷ : DecidableEq m
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq r
inst✝² : Field R
A₁₁ : Matrix m m R
A₁₂ : Matrix m n R
A₂₁ : Matrix n m R
A₂₂ : Matrix n n R
inst✝¹ : Invertible A₁₁
inst✝ : Invertible (A₂₂ - A₂₁ * ⅟A₁₁ * A₁₂)
this : Invertible (A₁₁.fromBlocks A₁₂ A₂₁ A₂₂) := A₁₁.fromBlocks₁₁Invertible A₁₂ A₂₁ A₂₂
⊢ (A₁₁.fromBlocks A₁₂ A₂₁ A₂₂)⁻¹ = ⅟(A₁₁.fromBlocks A₁₂ A₂₁ A₂₂)
Tactic:
rw [invOf_eq_nonsing_inv]
Proof state after:
no goals
Theorem: MatrixCookbook.eq_401
Proof state before:
R : Type u_2
l : Type ?u.78563
m : Type u_1
n : Type u_3
p : Type ?u.78572
q : Type ?u.78575
r : Type ?u.78578
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
A₁₁ : Matrix m m R
A₂₂ : Matrix n n R
h : IsUnit A₁₁ ↔ IsUnit A₂₂
⊢ A₁₁⁻¹.fromBlocks 0 (-(A₂₂⁻¹ * 0 * A₁₁⁻¹)) A₂₂⁻¹ = A₁₁⁻¹.fromBlocks 0 0 A₂₂⁻¹
Tactic:
simp
Proof state after:
no goals
Theorem: MatrixCookbook.eq_418
Proof state before:
R : Type u_1
l : Type ?u.93293
m : Type u_2
n✝ : Type ?u.93299
p : Type ?u.93302
q : Type ?u.93305
r : Type ?u.93308
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n✝
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n✝
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
A B : Matrix m m R
hA : IsIdempotentElem A
n : ℕ
hn : n ≠ 0
⊢ A ^ n = A
Tactic:
cases' n with n
Proof state after:
case zero
R : Type u_1
l : Type ?u.93293
m : Type u_2
n : Type ?u.93299
p : Type ?u.93302
q : Type ?u.93305
r : Type ?u.93308
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
A B : Matrix m m R
hA : IsIdempotentElem A
hn : 0 ≠ 0
⊢ A ^ 0 = A

case succ
R : Type u_1
l : Type ?u.93293
m : Type u_2
n✝ : Type ?u.93299
p : Type ?u.93302
q : Type ?u.93305
r : Type ?u.93308
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n✝
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n✝
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
A B : Matrix m m R
hA : IsIdempotentElem A
n : ℕ
hn : n + 1 ≠ 0
⊢ A ^ (n + 1) = A
Theorem: MatrixCookbook.eq_418
Proof state before:
case zero
R : Type u_1
l : Type ?u.93293
m : Type u_2
n : Type ?u.93299
p : Type ?u.93302
q : Type ?u.93305
r : Type ?u.93308
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
A B : Matrix m m R
hA : IsIdempotentElem A
hn : 0 ≠ 0
⊢ A ^ 0 = A
Tactic:
cases hn rfl
Proof state after:
no goals
Theorem: MatrixCookbook.eq_418
Proof state before:
case succ
R : Type u_1
l : Type ?u.93293
m : Type u_2
n✝ : Type ?u.93299
p : Type ?u.93302
q : Type ?u.93305
r : Type ?u.93308
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n✝
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n✝
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
A B : Matrix m m R
hA : IsIdempotentElem A
n : ℕ
hn : n + 1 ≠ 0
⊢ A ^ (n + 1) = A
Tactic:
exact hA.pow_succ_eq n
Proof state after:
no goals
Theorem: MatrixCookbook.eq_424
Proof state before:
R : Type u_1
l : Type ?u.105648
m : Type u_2
n : Type ?u.105654
p : Type ?u.105657
q : Type ?u.105660
r : Type ?u.105663
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
A B : Matrix m m R
hA : IsIdempotentElem A
⊢ A * (1 - A) = 0
Tactic:
rw [Matrix.mul_sub, Matrix.mul_one, hA.eq, sub_self]
Proof state after:
no goals
Theorem: MatrixCookbook.eq_425
Proof state before:
R : Type u_1
l : Type ?u.111522
m : Type u_2
n : Type ?u.111528
p : Type ?u.111531
q : Type ?u.111534
r : Type ?u.111537
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
A B : Matrix m m R
hA : IsIdempotentElem A
⊢ (1 - A) * A = 0
Tactic:
rw [Matrix.sub_mul, Matrix.one_mul, hA.eq, sub_self]
Proof state after:
no goals
Theorem: MatrixCookbook.eq_443
Proof state before:
R : Type ?u.119654
l : Type ?u.119657
m : Type ?u.119660
n : Type ?u.119663
p : Type ?u.119666
q : Type ?u.119669
r : Type ?u.119672
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
⊢ stdBasisMatrix 1 2 1 = of ![![0, 0, 0, 0], ![0, 0, 1, 0], ![0, 0, 0, 0], ![0, 0, 0, 0]]
Tactic:
decide
Proof state after:
no goals
Theorem: MatrixCookbook.eq_446
Proof state before:
R : Type u_3
l✝ : Type u_1
m : Type u_2
n : Type u_4
p : Type u_5
q : Type ?u.131057
r : Type ?u.131060
inst✝¹² : Fintype l✝
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l✝
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
A : Matrix l✝ m R
B : Matrix n p R
k : l✝
i : m
j : n
l : p
⊢ A k i * B j l = (A * stdBasisMatrix i j 1 * B) k l
Tactic:
sorry
Proof state after:
no goals
Theorem: MatrixCookbook.eq_447
Proof state before:
R : Type u_3
l✝ : Type u_1
m : Type u_2
n : Type u_4
p : Type u_5
q : Type ?u.134830
r : Type ?u.134833
inst✝¹² : Fintype l✝
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l✝
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
A : Matrix l✝ m R
B : Matrix n p R
k : m
i : l✝
j : p
l : n
⊢ A i k * B l j = (Aᵀ * stdBasisMatrix i j 1 * Bᵀ) k l
Tactic:
rw [←eq_446]
Proof state after:
R : Type u_3
l✝ : Type u_1
m : Type u_2
n : Type u_4
p : Type u_5
q : Type ?u.134830
r : Type ?u.134833
inst✝¹² : Fintype l✝
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l✝
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
A : Matrix l✝ m R
B : Matrix n p R
k : m
i : l✝
j : p
l : n
⊢ A i k * B l j = Aᵀ k i * Bᵀ j l
Theorem: MatrixCookbook.eq_447
Proof state before:
R : Type u_3
l✝ : Type u_1
m : Type u_2
n : Type u_4
p : Type u_5
q : Type ?u.134830
r : Type ?u.134833
inst✝¹² : Fintype l✝
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l✝
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
A : Matrix l✝ m R
B : Matrix n p R
k : m
i : l✝
j : p
l : n
⊢ A i k * B l j = Aᵀ k i * Bᵀ j l
Tactic:
rfl
Proof state after:
no goals
Theorem: MatrixCookbook.eq_448
Proof state before:
R : Type u_3
l✝ : Type u_1
m : Type u_2
n : Type u_4
p : Type u_5
q : Type ?u.139970
r : Type ?u.139973
inst✝¹² : Fintype l✝
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l✝
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
A : Matrix l✝ m R
B : Matrix n p R
k : m
i : l✝
j : n
l : p
⊢ A i k * B j l = (Aᵀ * stdBasisMatrix i j 1 * B) k l
Tactic:
rw [←eq_446]
Proof state after:
R : Type u_3
l✝ : Type u_1
m : Type u_2
n : Type u_4
p : Type u_5
q : Type ?u.139970
r : Type ?u.139973
inst✝¹² : Fintype l✝
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l✝
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
A : Matrix l✝ m R
B : Matrix n p R
k : m
i : l✝
j : n
l : p
⊢ A i k * B j l = Aᵀ k i * B j l
Theorem: MatrixCookbook.eq_448
Proof state before:
R : Type u_3
l✝ : Type u_1
m : Type u_2
n : Type u_4
p : Type u_5
q : Type ?u.139970
r : Type ?u.139973
inst✝¹² : Fintype l✝
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l✝
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
A : Matrix l✝ m R
B : Matrix n p R
k : m
i : l✝
j : n
l : p
⊢ A i k * B j l = Aᵀ k i * B j l
Tactic:
rfl
Proof state after:
no goals
Theorem: MatrixCookbook.eq_449
Proof state before:
R : Type u_3
l✝ : Type u_1
m : Type u_2
n : Type u_4
p : Type u_5
q : Type ?u.145108
r : Type ?u.145111
inst✝¹² : Fintype l✝
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l✝
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
A : Matrix l✝ m R
B : Matrix n p R
k : l✝
i : m
j : p
l : n
⊢ A k i * B l j = (A * stdBasisMatrix i j 1 * Bᵀ) k l
Tactic:
rw [←eq_446]
Proof state after:
R : Type u_3
l✝ : Type u_1
m : Type u_2
n : Type u_4
p : Type u_5
q : Type ?u.145108
r : Type ?u.145111
inst✝¹² : Fintype l✝
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l✝
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
A : Matrix l✝ m R
B : Matrix n p R
k : l✝
i : m
j : p
l : n
⊢ A k i * B l j = A k i * Bᵀ j l
Theorem: MatrixCookbook.eq_449
Proof state before:
R : Type u_3
l✝ : Type u_1
m : Type u_2
n : Type u_4
p : Type u_5
q : Type ?u.145108
r : Type ?u.145111
inst✝¹² : Fintype l✝
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l✝
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
A : Matrix l✝ m R
B : Matrix n p R
k : l✝
i : m
j : p
l : n
⊢ A k i * B l j = A k i * Bᵀ j l
Tactic:
rfl
Proof state after:
no goals
Theorem: MatrixCookbook.eq_461
Proof state before:
R : Type u_2
l : Type ?u.191294
m : Type u_1
n : Type ?u.191300
p : Type ?u.191303
q : Type ?u.191306
r : Type ?u.191309
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
A : Matrix m m R
hA : A = -Aᵀ
⊢ Aᵀ.det = (-1) ^ Fintype.card m * A.det
Tactic:
rw [hA, transpose_neg, transpose_transpose, det_neg, ← hA]
Proof state after:
no goals
Theorem: MatrixCookbook.eq_477
Proof state before:
R : Type u_1
l : Type ?u.198937
m : Type ?u.198940
n : Type ?u.198943
p : Type ?u.198946
q : Type ?u.198949
r : Type ?u.198952
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
⊢ of ![![0, 1, 0], ![1, 0, 0], ![0, 0, 1]] = of ![Pi.single 1 1, Pi.single 0 1, Pi.single 2 1]
Tactic:
ext i j
Proof state after:
case a
R : Type u_1
l : Type ?u.198937
m : Type ?u.198940
n : Type ?u.198943
p : Type ?u.198946
q : Type ?u.198949
r : Type ?u.198952
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
i j : Fin 3
⊢ of ![![0, 1, 0], ![1, 0, 0], ![0, 0, 1]] i j = of ![Pi.single 1 1, Pi.single 0 1, Pi.single 2 1] i j
Theorem: MatrixCookbook.eq_477
Proof state before:
case a
R : Type u_1
l : Type ?u.198937
m : Type ?u.198940
n : Type ?u.198943
p : Type ?u.198946
q : Type ?u.198949
r : Type ?u.198952
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
i j : Fin 3
⊢ of ![![0, 1, 0], ![1, 0, 0], ![0, 0, 1]] i j = of ![Pi.single 1 1, Pi.single 0 1, Pi.single 2 1] i j
Tactic:
fin_cases i <;> fin_cases j <;> rfl
Proof state after:
no goals
Theorem: MatrixCookbook.eq_478
Proof state before:
R : Type u_2
l : Type ?u.206287
m : Type u_1
n : Type ?u.206293
p : Type ?u.206296
q : Type ?u.206299
r : Type ?u.206302
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
e : Equiv.Perm m
⊢ (Equiv.toPEquiv e).toMatrix * (Equiv.toPEquiv e).toMatrixᵀ = 1
Tactic:
rw [← PEquiv.toMatrix_symm, ← PEquiv.toMatrix_trans, ← Equiv.toPEquiv_symm, ←
  Equiv.toPEquiv_trans, Equiv.self_trans_symm, Equiv.toPEquiv_refl, PEquiv.toMatrix_refl]
Proof state after:
no goals
Theorem: MatrixCookbook.eq_151
Proof state before:
m : Type ?u.9800
n : Type u_1
p : Type ?u.9806
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : Fintype p
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq p
A B C : Matrix n n ℂ
⊢ A⁻¹ = (1 / A.det) • A.adjugate
Tactic:
rw [inv_def, Ring.inverse_eq_inv, one_div]
Proof state after:
no goals
Theorem: MatrixCookbook.eq_160
Proof state before:
m : Type ?u.18898
n : Type u_1
p : Type ?u.18904
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : Fintype p
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq p
A B C : Matrix n n ℂ
b c : n → ℂ
⊢ (A + col b * row c)⁻¹ = A⁻¹ - (1 + c ⬝ᵥ A⁻¹ *ᵥ b)⁻¹ • A⁻¹ * (col b * row c) * A⁻¹
Tactic:
rw [eq_159, ← Matrix.mul_assoc _ (col b), Matrix.mul_assoc _ (row c), Matrix.mul_assoc _ (row c),
  Matrix.smul_mul]
Proof state after:
m : Type ?u.18898
n : Type u_1
p : Type ?u.18904
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : Fintype p
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq p
A B C : Matrix n n ℂ
b c : n → ℂ
⊢ A⁻¹ - A⁻¹ * col b * (1 + row c * A⁻¹ * col b)⁻¹ * (row c * A⁻¹) =
    A⁻¹ - (1 + c ⬝ᵥ A⁻¹ *ᵥ b)⁻¹ • (A⁻¹ * col b) * (row c * A⁻¹)
Theorem: MatrixCookbook.eq_160
Proof state before:
m : Type ?u.18898
n : Type u_1
p : Type ?u.18904
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : Fintype p
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq p
A B C : Matrix n n ℂ
b c : n → ℂ
⊢ A⁻¹ - A⁻¹ * col b * (1 + row c * A⁻¹ * col b)⁻¹ * (row c * A⁻¹) =
    A⁻¹ - (1 + c ⬝ᵥ A⁻¹ *ᵥ b)⁻¹ • (A⁻¹ * col b) * (row c * A⁻¹)
Tactic:
congr
Proof state after:
case e_a.e_a
m : Type ?u.18898
n : Type u_1
p : Type ?u.18904
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : Fintype p
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq p
A B C : Matrix n n ℂ
b c : n → ℂ
⊢ A⁻¹ * col b * (1 + row c * A⁻¹ * col b)⁻¹ = (1 + c ⬝ᵥ A⁻¹ *ᵥ b)⁻¹ • (A⁻¹ * col b)
Theorem: MatrixCookbook.eq_160
Proof state before:
case e_a.e_a
m : Type ?u.18898
n : Type u_1
p : Type ?u.18904
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : Fintype p
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq p
A B C : Matrix n n ℂ
b c : n → ℂ
⊢ A⁻¹ * col b * (1 + row c * A⁻¹ * col b)⁻¹ = (1 + c ⬝ᵥ A⁻¹ *ᵥ b)⁻¹ • (A⁻¹ * col b)
Tactic:
sorry
Proof state after:
no goals
Theorem: MatrixCookbook.eq_163
Proof state before:
m : Type ?u.28189
n : Type u_1
p : Type ?u.28195
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : Fintype p
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq p
A B C : Matrix n n ℂ
hA : IsUnit A
hB : IsUnit B
⊢ (A⁻¹ + B⁻¹)⁻¹ = A * (A + B)⁻¹ * B ∧ (A⁻¹ + B⁻¹)⁻¹ = B * (A + B)⁻¹ * A
Tactic:
letI := hA.invertible
Proof state after:
m : Type ?u.28189
n : Type u_1
p : Type ?u.28195
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : Fintype p
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq p
A B C : Matrix n n ℂ
hA : IsUnit A
hB : IsUnit B
this : Invertible A := hA.invertible
⊢ (A⁻¹ + B⁻¹)⁻¹ = A * (A + B)⁻¹ * B ∧ (A⁻¹ + B⁻¹)⁻¹ = B * (A + B)⁻¹ * A
Theorem: MatrixCookbook.eq_163
Proof state before:
m : Type ?u.28189
n : Type u_1
p : Type ?u.28195
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : Fintype p
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq p
A B C : Matrix n n ℂ
hA : IsUnit A
hB : IsUnit B
this : Invertible A := hA.invertible
⊢ (A⁻¹ + B⁻¹)⁻¹ = A * (A + B)⁻¹ * B ∧ (A⁻¹ + B⁻¹)⁻¹ = B * (A + B)⁻¹ * A
Tactic:
letI := hB.invertible
Proof state after:
m : Type ?u.28189
n : Type u_1
p : Type ?u.28195
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : Fintype p
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq p
A B C : Matrix n n ℂ
hA : IsUnit A
hB : IsUnit B
this✝ : Invertible A := hA.invertible
this : Invertible B := hB.invertible
⊢ (A⁻¹ + B⁻¹)⁻¹ = A * (A + B)⁻¹ * B ∧ (A⁻¹ + B⁻¹)⁻¹ = B * (A + B)⁻¹ * A