ι : Type u_3
ι' : Type ?u.1468229
𝕜 : Type u_1
inst✝¹⁰ : IsROrC 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.1468258
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.1468276
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.1468296
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a b : OrthonormalBasis ι 𝕜 E
this : ↑(↑normSq (↑(Basis.det (OrthonormalBasis.toBasis a)) ↑b)) = 1
⊢ ‖↑(Basis.det (OrthonormalBasis.toBasis a)) ↑b‖ = 1
ι : Type u_3
ι' : Type ?u.1468229
𝕜 : Type u_1
inst✝¹⁰ : IsROrC 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.1468258
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.1468276
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.1468296
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a b : OrthonormalBasis ι 𝕜 E
⊢ ‖↑(Basis.det (OrthonormalBasis.toBasis a)) ↑b‖ = 1
have : (normSq (a.toBasis.det b) : 𝕜) = 1 := by
  simpa [IsROrC.mul_conj] using
    (Matrix.det_of_mem_unitary (a.toMatrix_orthonormalBasis_mem_unitary b)).2
ι : Type u_3
ι' : Type ?u.1468229
𝕜 : Type u_1
inst✝¹⁰ : IsROrC 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.1468258
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.1468276
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.1468296
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a b : OrthonormalBasis ι 𝕜 E
this : ↑normSq (↑(Basis.det (OrthonormalBasis.toBasis a)) ↑b) = 1
⊢ ‖↑(Basis.det (OrthonormalBasis.toBasis a)) ↑b‖ = 1
ι : Type u_3
ι' : Type ?u.1468229
𝕜 : Type u_1
inst✝¹⁰ : IsROrC 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.1468258
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.1468276
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.1468296
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a b : OrthonormalBasis ι 𝕜 E
this : ↑(↑normSq (↑(Basis.det (OrthonormalBasis.toBasis a)) ↑b)) = 1
⊢ ‖↑(Basis.det (OrthonormalBasis.toBasis a)) ↑b‖ = 1
norm_cast at this
no goals
ι : Type u_3
ι' : Type ?u.1468229
𝕜 : Type u_1
inst✝¹⁰ : IsROrC 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.1468258
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.1468276
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.1468296
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a b : OrthonormalBasis ι 𝕜 E
this : ↑normSq (↑(Basis.det (OrthonormalBasis.toBasis a)) ↑b) = 1
⊢ ‖↑(Basis.det (OrthonormalBasis.toBasis a)) ↑b‖ = 1
rwa [← sqrt_normSq_eq_norm, sqrt_eq_one]
no goals
ι : Type u_3
ι' : Type ?u.1468229
𝕜 : Type u_1
inst✝¹⁰ : IsROrC 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.1468258
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.1468276
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.1468296
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a b : OrthonormalBasis ι 𝕜 E
⊢ ↑(↑normSq (↑(Basis.det (OrthonormalBasis.toBasis a)) ↑b)) = 1
simpa [IsROrC.mul_conj] using
  (Matrix.det_of_mem_unitary (a.toMatrix_orthonormalBasis_mem_unitary b)).2