no goals
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type ?u.1528607
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e✝ : Basis ι R M
f : M ≃ₗ[R] M
e : M ≃ₗ[R] M'
⊢ ↑LinearEquiv.det (trans (trans (symm e) f) e) = ↑LinearEquiv.det f
rw [← Units.eq_iff, coe_det, coe_det, ← comp_coe, ← comp_coe, LinearMap.det_conj]