ι : Type u_2
ι' : Type ?u.1554527
𝕜 : Type ?u.1554530
inst✝¹⁰ : IsROrC 𝕜
E : Type ?u.1554536
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.1554556
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type u_1
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.1554594
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a b : OrthonormalBasis ι ℝ F
⊢ ↑(Basis.det (OrthonormalBasis.toBasis a)) ↑b ^ 2 = 1
ι : Type u_2
ι' : Type ?u.1554527
𝕜 : Type ?u.1554530
inst✝¹⁰ : IsROrC 𝕜
E : Type ?u.1554536
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.1554556
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type u_1
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.1554594
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a b : OrthonormalBasis ι ℝ F
⊢ ↑(Basis.det (OrthonormalBasis.toBasis a)) ↑b = 1 ∨ ↑(Basis.det (OrthonormalBasis.toBasis a)) ↑b = -1
rw [← sq_eq_one_iff]
no goals
ι : Type u_2
ι' : Type ?u.1554527
𝕜 : Type ?u.1554530
inst✝¹⁰ : IsROrC 𝕜
E : Type ?u.1554536
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.1554556
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type u_1
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.1554594
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a b : OrthonormalBasis ι ℝ F
⊢ ↑(Basis.det (OrthonormalBasis.toBasis a)) ↑b ^ 2 = 1
simpa [unitary, sq] using Matrix.det_of_mem_unitary (a.toMatrix_orthonormalBasis_mem_unitary b)