no goals
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type ?u.2527336
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
⊢ ↑(det e) ↑e = 1
simp [e.det_apply]