no goals
R : Type u_1
inst✝⁷ : CommRing R
M : Type u_2
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type ?u.2545400
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
ι : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
e : Basis ι R M
inst✝ : Nontrivial R
h : det e = 0
⊢ False
simpa [h] using e.det_self