Theorem: MatrixCookbook.eq_447 (MatrixCookbook/9SpecialMatrices.lean)

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]
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

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
State after:
no goals