no goals
R : Type ?u.466824
inst✝¹¹ : CommRing R
M : Type ?u.466830
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
M' : Type ?u.467415
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R M'
ι✝ : Type ?u.467957
inst✝⁶ : DecidableEq ι✝
inst✝⁵ : Fintype ι✝
e : Basis ι✝ R M
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Module A M
κ : Type ?u.468933
inst✝² : Fintype κ
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : (ι → A) →ₗ[A] ι → A
⊢ det (↑toMatrix' f) = ↑LinearMap.det f
simp [← toMatrix_eq_toMatrix']