case inl
R : Type u_1
inst✝³ : LinearOrderedField R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : Fintype ι
_i : FiniteDimensional R M
x : Orientation R M ι
f : M ≃ₗ[R] M
h : Fintype.card ι = finrank R M
h✝ : IsEmpty ι
⊢ ↑(map ι f) x = x ↔ 0 < ↑LinearMap.det ↑f

case inr
R : Type u_1
inst✝³ : LinearOrderedField R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : Fintype ι
_i : FiniteDimensional R M
x : Orientation R M ι
f : M ≃ₗ[R] M
h : Fintype.card ι = finrank R M
h✝ : Nonempty ι
⊢ ↑(map ι f) x = x ↔ 0 < ↑LinearMap.det ↑f
R : Type u_1
inst✝³ : LinearOrderedField R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : Fintype ι
_i : FiniteDimensional R M
x : Orientation R M ι
f : M ≃ₗ[R] M
h : Fintype.card ι = finrank R M
⊢ ↑(map ι f) x = x ↔ 0 < ↑LinearMap.det ↑f
cases isEmpty_or_nonempty ι
no goals
case inr
R : Type u_1
inst✝³ : LinearOrderedField R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : Fintype ι
_i : FiniteDimensional R M
x : Orientation R M ι
f : M ≃ₗ[R] M
h : Fintype.card ι = finrank R M
h✝ : Nonempty ι
⊢ ↑(map ι f) x = x ↔ 0 < ↑LinearMap.det ↑f
rw [map_eq_det_inv_smul _ _ h, units_inv_smul, units_smul_eq_self_iff, LinearEquiv.coe_det]
case inl
R : Type u_1
inst✝³ : LinearOrderedField R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : Fintype ι
_i : FiniteDimensional R M
x : Orientation R M ι
f : M ≃ₗ[R] M
h : Fintype.card ι = finrank R M
h✝ : IsEmpty ι
H : finrank R M = 0
⊢ ↑(map ι f) x = x ↔ 0 < ↑LinearMap.det ↑f
case inl
R : Type u_1
inst✝³ : LinearOrderedField R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : Fintype ι
_i : FiniteDimensional R M
x : Orientation R M ι
f : M ≃ₗ[R] M
h : Fintype.card ι = finrank R M
h✝ : IsEmpty ι
⊢ ↑(map ι f) x = x ↔ 0 < ↑LinearMap.det ↑f
have H : finrank R M = 0 := by
  refine' h.symm.trans _
  convert @Fintype.card_of_isEmpty ι _
no goals
case inl
R : Type u_1
inst✝³ : LinearOrderedField R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : Fintype ι
_i : FiniteDimensional R M
x : Orientation R M ι
f : M ≃ₗ[R] M
h : Fintype.card ι = finrank R M
h✝ : IsEmpty ι
H : finrank R M = 0
⊢ ↑(map ι f) x = x ↔ 0 < ↑LinearMap.det ↑f
simp [LinearMap.det_eq_one_of_finrank_eq_zero H]
R : Type u_1
inst✝³ : LinearOrderedField R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : Fintype ι
_i : FiniteDimensional R M
x : Orientation R M ι
f : M ≃ₗ[R] M
h : Fintype.card ι = finrank R M
h✝ : IsEmpty ι
⊢ Fintype.card ι = 0
R : Type u_1
inst✝³ : LinearOrderedField R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : Fintype ι
_i : FiniteDimensional R M
x : Orientation R M ι
f : M ≃ₗ[R] M
h : Fintype.card ι = finrank R M
h✝ : IsEmpty ι
⊢ finrank R M = 0
refine' h.symm.trans _
no goals
R : Type u_1
inst✝³ : LinearOrderedField R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : Fintype ι
_i : FiniteDimensional R M
x : Orientation R M ι
f : M ≃ₗ[R] M
h : Fintype.card ι = finrank R M
h✝ : IsEmpty ι
⊢ Fintype.card ι = 0
convert @Fintype.card_of_isEmpty ι _