E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
ne : Nonempty ι
e f : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
h : ↑(Basis.det (OrthonormalBasis.toBasis e)) ↑f ≠ -1
⊢ Basis.orientation (OrthonormalBasis.toBasis e) = Basis.orientation (OrthonormalBasis.toBasis f)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
ne : Nonempty ι
e f : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
h : Basis.orientation (OrthonormalBasis.toBasis e) ≠ Basis.orientation (OrthonormalBasis.toBasis f)
⊢ ↑(Basis.det (OrthonormalBasis.toBasis e)) ↑f = -1
contrapose! h
no goals
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
ne : Nonempty ι
e f : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
h : ↑(Basis.det (OrthonormalBasis.toBasis e)) ↑f ≠ -1
⊢ Basis.orientation (OrthonormalBasis.toBasis e) = Basis.orientation (OrthonormalBasis.toBasis f)
simp [e.toBasis.orientation_eq_iff_det_pos,
  (e.det_to_matrix_orthonormalBasis_real f).resolve_right h]