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)) ↑(OrthonormalBasis.toBasis f) • Basis.det (OrthonormalBasis.toBasis f) =
    -Basis.det (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) = -Basis.det (OrthonormalBasis.toBasis f)
rw [e.toBasis.det.eq_smul_basis_det f.toBasis]
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.orientation (OrthonormalBasis.toBasis e) ≠ Basis.orientation (OrthonormalBasis.toBasis f)
⊢ ↑(Basis.det (OrthonormalBasis.toBasis e)) ↑(OrthonormalBasis.toBasis f) • Basis.det (OrthonormalBasis.toBasis f) =
    -Basis.det (OrthonormalBasis.toBasis f)
simp [e.det_to_matrix_orthonormalBasis_of_opposite_orientation f h,
  neg_one_smul ℝ (M := AlternatingMap ℝ E ℝ ι)]