no goals
R : Type u_2
inst✝⁸ : CommRing R
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
M' : Type u_4
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
ι : Type u_1
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
e : Basis ι R M
A : Type ?u.2708089
inst✝¹ : CommRing A
inst✝ : Module A M
b : Basis ι R M
f : M ≃ₗ[R] M'
v : ι → M'
⊢ ↑(det (Basis.map b f)) v = ↑(det b) (↑(LinearEquiv.symm f) ∘ v)
rw [Basis.det_apply, Basis.toMatrix_map, Basis.det_apply]