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

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