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

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