no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.739707
G : Type ?u.739710
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace F
A : E →L[𝕜] E
x : E
⊢ ‖↑A x‖ = Real.sqrt (↑re (inner x (↑(↑adjoint A * A) x)))
rw [← apply_norm_sq_eq_inner_adjoint_right, Real.sqrt_sq (norm_nonneg _)]