no goals
R : Type u_3
inst✝¹⁰ : CommRing R
M : Type u_4
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
M' : Type ?u.2702037
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
e✝ : Basis ι R M
A : Type ?u.2703057
inst✝³ : CommRing A
inst✝² : Module A M
ι' : Type u_1
inst✝¹ : Fintype ι'
inst✝ : DecidableEq ι'
b : Basis ι R M
v : ι → M
e : ι' ≃ ι
⊢ ↑(det (reindex b e.symm)) (v ∘ ↑e) = ↑(det b) v
rw [Basis.det_reindex, Function.comp.assoc, e.self_comp_symm, Function.comp.right_id]