(T : F →L[ℂ] F) (hT : IsSelfAdjoint T) (x : F) : (((inner ℂ (T x) x : ℂ).re : ℝ) : ℂ) = inner ℂ (T x) x

Initializing...

(T : F →L[ℂ] F) (hT : IsSelfAdjoint T) (x : F) : (((inner ℂ (T x) x : ℂ).re : ℝ) : ℂ) = inner ℂ (T x) x · Prove2Me