R : Type ?u.871535
inst✝¹¹ : CommRing R
M : Type u_3
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
M' : Type ?u.872126
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R M'
ι✝ : Type ?u.872668
inst✝⁶ : DecidableEq ι✝
inst✝⁵ : Fintype ι✝
e : Basis ι✝ R M
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Module A M
κ : Type ?u.873644
inst✝² : Fintype κ
ι : Type u_1
inst✝¹ : Finite ι
inst✝ : Nonempty ι
b : Basis ι A M
this : DecidableEq ι
⊢ ↑LinearMap.det 0 = 0
R : Type ?u.871535
inst✝¹¹ : CommRing R
M : Type u_3
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
M' : Type ?u.872126
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R M'
ι✝ : Type ?u.872668
inst✝⁶ : DecidableEq ι✝
inst✝⁵ : Fintype ι✝
e : Basis ι✝ R M
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Module A M
κ : Type ?u.873644
inst✝² : Fintype κ
ι : Type u_1
inst✝¹ : Finite ι
inst✝ : Nonempty ι
b : Basis ι A M
⊢ ↑LinearMap.det 0 = 0
haveI := Classical.decEq ι
case intro
R : Type ?u.871535
inst✝¹¹ : CommRing R
M : Type u_3
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
M' : Type ?u.872126
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R M'
ι✝ : Type ?u.872668
inst✝⁶ : DecidableEq ι✝
inst✝⁵ : Fintype ι✝
e : Basis ι✝ R M
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Module A M
κ : Type ?u.873644
inst✝² : Fintype κ
ι : Type u_1
inst✝¹ : Finite ι
inst✝ : Nonempty ι
b : Basis ι A M
this : DecidableEq ι
val✝ : Fintype ι
⊢ ↑LinearMap.det 0 = 0
R : Type ?u.871535
inst✝¹¹ : CommRing R
M : Type u_3
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
M' : Type ?u.872126
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R M'
ι✝ : Type ?u.872668
inst✝⁶ : DecidableEq ι✝
inst✝⁵ : Fintype ι✝
e : Basis ι✝ R M
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Module A M
κ : Type ?u.873644
inst✝² : Fintype κ
ι : Type u_1
inst✝¹ : Finite ι
inst✝ : Nonempty ι
b : Basis ι A M
this : DecidableEq ι
⊢ ↑LinearMap.det 0 = 0
cases nonempty_fintype ι
no goals
case intro
R : Type ?u.871535
inst✝¹¹ : CommRing R
M : Type u_3
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
M' : Type ?u.872126
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R M'
ι✝ : Type ?u.872668
inst✝⁶ : DecidableEq ι✝
inst✝⁵ : Fintype ι✝
e : Basis ι✝ R M
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Module A M
κ : Type ?u.873644
inst✝² : Fintype κ
ι : Type u_1
inst✝¹ : Finite ι
inst✝ : Nonempty ι
b : Basis ι A M
this : DecidableEq ι
val✝ : Fintype ι
⊢ ↑LinearMap.det 0 = 0
rwa [← det_toMatrix b, LinearEquiv.map_zero, det_zero]