case intro
R : Type u_2
inst✝⁷ : CommRing R
M : Type u_3
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type ?u.2607358
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
ι✝ : Type ?u.2607900
inst✝² : DecidableEq ι✝
inst✝¹ : Fintype ι✝
e✝ : Basis ι✝ R M
ι : Type u_1
inst✝ : Finite ι
e : Basis ι R M
f : AlternatingMap R M R ι
h : ↑f ↑e = 0
val✝ : Fintype ι
⊢ f = 0
R : Type u_2
inst✝⁷ : CommRing R
M : Type u_3
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type ?u.2607358
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
ι✝ : Type ?u.2607900
inst✝² : DecidableEq ι✝
inst✝¹ : Fintype ι✝
e✝ : Basis ι✝ R M
ι : Type u_1
inst✝ : Finite ι
e : Basis ι R M
f : AlternatingMap R M R ι
h : ↑f ↑e = 0
⊢ f = 0
cases nonempty_fintype ι
case intro
R : Type u_2
inst✝⁷ : CommRing R
M : Type u_3
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type ?u.2607358
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
ι✝ : Type ?u.2607900
inst✝² : DecidableEq ι✝
inst✝¹ : Fintype ι✝
e✝ : Basis ι✝ R M
ι : Type u_1
inst✝ : Finite ι
e : Basis ι R M
f : AlternatingMap R M R ι
h : ↑f ↑e = 0
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
⊢ f = 0
case intro
R : Type u_2
inst✝⁷ : CommRing R
M : Type u_3
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type ?u.2607358
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
ι✝ : Type ?u.2607900
inst✝² : DecidableEq ι✝
inst✝¹ : Fintype ι✝
e✝ : Basis ι✝ R M
ι : Type u_1
inst✝ : Finite ι
e : Basis ι R M
f : AlternatingMap R M R ι
h : ↑f ↑e = 0
val✝ : Fintype ι
⊢ f = 0
letI := Classical.decEq ι
no goals
case intro
R : Type u_2
inst✝⁷ : CommRing R
M : Type u_3
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type ?u.2607358
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
ι✝ : Type ?u.2607900
inst✝² : DecidableEq ι✝
inst✝¹ : Fintype ι✝
e✝ : Basis ι✝ R M
ι : Type u_1
inst✝ : Finite ι
e : Basis ι R M
f : AlternatingMap R M R ι
h : ↑f ↑e = 0
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
⊢ f = 0
simpa [h] using f.eq_smul_basis_det e