some obvious lemmas on self-adjoint operators

This file provides the polarization identity for self adjoint continuous linear maps over is_R_or_C.

theorem ContinuousLinearMap.IsSelfAdjoint.inner_map_self_eq_zero {𝕜 : Type u_2} {E : Type u_1} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {T : E →L[𝕜] E} (hT : IsSelfAdjoint T) : (∀ (x : E), inner (T x) x = 0) ↔ T = 0

Given a self-adjoint continuous linear operator $T$ on $E$, we get $\langle T x, x \rangle = 0$ for any $x\in E$ if and only if $T=0$.

theorem ContinuousLinearMap.IsSelfAdjoint.inner_map_polarization {𝕜 : Type u_2} {E : Type u_1} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {T : E →L[𝕜] E} (hT : IsSelfAdjoint T) (x : E) (y : E) : inner (T x) y = (inner (T (x + y)) (x + y) - inner (T (x - y)) (x - y) - RCLike.I * inner (T (x + RCLike.I • y)) (x + RCLike.I • y) + RCLike.I * inner (T (x - RCLike.I • y)) (x - RCLike.I • y)) / 4

The polarization identity for self-adjoint operators.