no goals
R : Type ?u.1737265
inst✝⁸ : CommRing R
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
M' : Type ?u.1737856
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
ι : Type ?u.1738398
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
e : Basis ι R M
𝕜 : Type u_1
inst✝¹ : Field 𝕜
inst✝ : Module 𝕜 M
f : M ≃ₗ[𝕜] M
⊢ ↑LinearMap.det ↑(symm f) = (↑LinearMap.det ↑f)⁻¹
field_simp [IsUnit.ne_zero f.isUnit_det']