no goals
R : Type ?u.1634353
inst✝⁸ : CommRing R
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
M' : Type ?u.1634944
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
ι : Type ?u.1635486
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
e : Basis ι R M
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Module A M
f : M ≃ₗ[A] M
⊢ ↑LinearMap.det ↑(symm f) * ↑LinearMap.det ↑f = 1
simp [← LinearMap.det_comp]