no goals
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
i j : n
⊢ adjugate A i j = det (updateRow A j (Pi.single i 1))
rw [adjugate_def, of_apply, cramer_apply, updateColumn_transpose, det_transpose]