no goals
R : Type ?u.899641
inst✝¹² : CommRing R
M✝ : Type ?u.899647
inst✝¹¹ : AddCommGroup M✝
inst✝¹⁰ : Module R M✝
M' : Type ?u.900232
inst✝⁹ : AddCommGroup M'
inst✝⁸ : Module R M'
ι : Type ?u.900774
inst✝⁷ : DecidableEq ι
inst✝⁶ : Fintype ι
e : Basis ι R M✝
A : Type ?u.901252
inst✝⁵ : CommRing A
inst✝⁴ : Module A M✝
κ : Type ?u.901750
inst✝³ : Fintype κ
𝕜 : Type u_1
inst✝² : Field 𝕜
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
⊢ ↑LinearMap.det 0 = 0 ^ FiniteDimensional.finrank 𝕜 M
simp only [← zero_smul 𝕜 (1 : M →ₗ[𝕜] M), det_smul, mul_one, MonoidHom.map_one]