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 α
b : n → α
i : n
⊢ ↑(cramer Aᵀ) b i = det (updateRow A i b)
rw [cramer_apply, updateColumn_transpose, det_transpose]