R : Type u_1
inst✝⁸ : StrictOrderedCommRing R
M : Type u_3
N : Type ?u.117323
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : Nontrivial R
inst✝ : IsEmpty ι
b : Basis ι R M
⊢ rayOfNeZero R (det b) (_ : det b ≠ 0) = positiveOrientation
R : Type u_1
inst✝⁸ : StrictOrderedCommRing R
M : Type u_3
N : Type ?u.117323
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : Nontrivial R
inst✝ : IsEmpty ι
b : Basis ι R M
⊢ Basis.orientation b = positiveOrientation
rw [Basis.orientation]
case e_v
R : Type u_1
inst✝⁸ : StrictOrderedCommRing R
M : Type u_3
N : Type ?u.117323
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : Nontrivial R
inst✝ : IsEmpty ι
b : Basis ι R M
⊢ det b = ↑AlternatingMap.constLinearEquivOfIsEmpty 1
R : Type u_1
inst✝⁸ : StrictOrderedCommRing R
M : Type u_3
N : Type ?u.117323
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : Nontrivial R
inst✝ : IsEmpty ι
b : Basis ι R M
⊢ rayOfNeZero R (det b) (_ : det b ≠ 0) = positiveOrientation
congr
no goals
case e_v
R : Type u_1
inst✝⁸ : StrictOrderedCommRing R
M : Type u_3
N : Type ?u.117323
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : Nontrivial R
inst✝ : IsEmpty ι
b : Basis ι R M
⊢ det b = ↑AlternatingMap.constLinearEquivOfIsEmpty 1
exact b.det_isEmpty