rw [inv_def, Ring.inverse_eq_inv, one_div]
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
no goals