(T : F →L[ℂ] F) (c : ℝ) (x : F) : (inner ℂ ((T - (algebraMap ℝ (F →L[ℂ] F)) c) x) x : ℂ).re = (inner ℂ (T x) x : ℂ).re

Initializing...

(T : F →L[ℂ] F) (c : ℝ) (x : F) : (inner ℂ ((T - (algebraMap ℝ (F →L[ℂ] F)) c) x) x : ℂ).re = (inner ℂ (T x) x : ℂ).re - c * ‖x‖ ^ 2 · Prove2Me