case H
R : Type u_2
inst✝⁷ : CommRing R
M : Type u_3
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type ?u.2538346
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
ι : Type u_1
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
e : Basis ι R M
inst✝ : IsEmpty ι
v : ι → M
⊢ ↑(det e) v = ↑(AlternatingMap.constOfIsEmpty R M ι 1) v
R : Type u_2
inst✝⁷ : CommRing R
M : Type u_3
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type ?u.2538346
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
ι : Type u_1
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
e : Basis ι R M
inst✝ : IsEmpty ι
⊢ det e = AlternatingMap.constOfIsEmpty R M ι 1
ext v
no goals
case H
R : Type u_2
inst✝⁷ : CommRing R
M : Type u_3
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M' : Type ?u.2538346
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
ι : Type u_1
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
e : Basis ι R M
inst✝ : IsEmpty ι
v : ι → M
⊢ ↑(det e) v = ↑(AlternatingMap.constOfIsEmpty R M ι 1) v
exact Matrix.det_isEmpty