Theorems · Definition · functional analysis

ContinuousLinearMap.reApplyInnerSelf

{𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : RCLike 𝕜] → [inst_1 : SeminormedAddCommGroup E] → [inst_2 : InnerProductSpace 𝕜 E] → (E →L[𝕜] E) → E → ℝ

Extract a real bilinear form from an operator T, by taking the pairing fun x ↦ re ⟪T x, x⟫.

Defined in

Mathlib.Analysis.InnerProductSpace.LinearMap

Cited by

17 results in Mathlib

Foundations

Depth 96 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RCLikeSeminormedAddCommGroupInnerProductSpace