toSesqForm — Mathlib

English

The flipped sesquilinear map satisfies innerSLFlip(x, y) = ⟪y, x⟫.

Русский

Разворотная сесклярная форма удовлетворяет innerSLFlip(x,y) = ⟪y,x⟫.

LaTeX

$$$ innerSLFlip 𝕜 x y = ⟪y, x⟫ $$$

Lean4

/-- Given `f : E →L[𝕜] E'`, construct the continuous sesquilinear form `fun x y ↦ ⟪x, A y⟫`, given
as a continuous linear map. -/
noncomputable def toSesqForm : (E →L[𝕜] E') →L[𝕜] E' →L⋆[𝕜] E →L[𝕜] 𝕜 :=
  (ContinuousLinearMap.flipₗᵢ' E E' 𝕜 (starRingEnd 𝕜) (RingHom.id 𝕜)).toContinuousLinearEquiv ∘L
    ContinuousLinearMap.compSL E E' (E' →L⋆[𝕜] 𝕜) (RingHom.id 𝕜) (RingHom.id 𝕜) (innerSLFlip 𝕜)

Похожие утверждения