{m : ℕ} (w : Fin m → E) (x : E) : (ContinuousLinearMap.adjoint (synthesis w)) x = (WithLp.toLp 2 fun i => ⟪w i, x⟫_ℂ)

Initializing...

{m : ℕ} (w : Fin m → E) (x : E) : (ContinuousLinearMap.adjoint (synthesis w)) x = (WithLp.toLp 2 fun i => ⟪w i, x⟫_ℂ) · Prove2Me