[GOAL]
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Free R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
⊢ ↑LinearMap.det 0 = 0
[PROOFSTEP]
letI : Nonempty (Module.Free.ChooseBasisIndex R M) := (Module.Free.chooseBasis R M).index_nonempty
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Free R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
this : Nonempty (Module.Free.ChooseBasisIndex R M) := Basis.index_nonempty (Module.Free.chooseBasis R M)
⊢ ↑LinearMap.det 0 = 0
[PROOFSTEP]
nontriviality R
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Free R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
this : Nonempty (Module.Free.ChooseBasisIndex R M) := Basis.index_nonempty (Module.Free.chooseBasis R M)
✝ : Nontrivial R
⊢ ↑LinearMap.det 0 = 0
[PROOFSTEP]
exact LinearMap.det_zero' (Module.Free.chooseBasis R M)
