no goals
R : Type u_2
inst✝⁹ : CommRing R
M : Type ?u.566367
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
M' : Type ?u.566952
inst✝⁶ : AddCommGroup M'
inst✝⁵ : Module R M'
ι : Type u_1
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
e : Basis ι R M
A : Type ?u.567972
inst✝² : CommRing A
inst✝¹ : Module A M
κ : Type ?u.568470
inst✝ : Fintype κ
f : Matrix ι ι R
⊢ ↑LinearMap.det (↑toLin' f) = det f
simp only [← toLin_eq_toLin', det_toLin]