Theorem: MatrixCookbook.eq_31 (MatrixCookbook/1Basic.lean)

State before:
ι : Type ?u.145147
R : Type u_1
m : Type ?u.145153
n : Type ?u.145156
p : Type ?u.145159
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Fintype p
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : Field R
A : Matrix (Fin 2) (Fin 2) R
⊢ A⁻¹ = A.det⁻¹ • of ![![A 1 1, -A 0 1], ![-A 1 0, A 0 0]]
Tactic:
rw [inv_def, adjugate_fin_two, Ring.inverse_eq_inv]
State after:
no goals