no goals
R : Type u_2
inst✝⁹ : CommRing R
M : Type u_3
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
M' : Type ?u.521225
inst✝⁶ : AddCommGroup M'
inst✝⁵ : Module R M'
ι : Type u_1
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
e : Basis ι R M
A : Type ?u.522245
inst✝² : CommRing A
inst✝¹ : Module A M
κ : Type ?u.522743
inst✝ : Fintype κ
b : Basis ι R M
f : Matrix ι ι R
⊢ ↑LinearMap.det (↑(toLin b b) f) = det f
rw [← LinearMap.det_toMatrix b, LinearMap.toMatrix_toLin]