Theorem: MatrixCookbook.eq_151 (MatrixCookbook/3Inverses.lean)

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