`BookProof.ChapterH7.inner_self_real` (X : E →L[ℂ] E) (hX : IsSelfAdjoint X) (x : E) : (inner ℂ x (X x) : ℂ).im = 0

Initializing...

`BookProof.ChapterH7.inner_self_real` (X : E →L[ℂ] E) (hX : IsSelfAdjoint X) (x : E) : (inner ℂ x (X x) : ℂ).im = 0 · Prove2Me