Adjoint operator for normed spaces

Stream: Is there code for X?

[Vasilii Nesterov]

Do we have something like

def dual {X Y 𝕜 : Type*} [NormedField 𝕜] [NormedAddCommGroup X] [NormedSpace 𝕜 X]
    [NormedAddCommGroup Y] [NormedSpace 𝕜 Y] (f : X →L[𝕜] Y) :
    StrongDual 𝕜 Y →L[𝕜] StrongDual 𝕜 X where
  toFun φ := ⟨φ ∘ₗ f.toLinearMap, sorry⟩
  map_add' := sorry
  map_smul' := sorry
  cont := sorry

for an adjoint operator in a normed space?

[Moritz Doll]

docs#ContinuousLinearMap.precomp

[Etienne Marion]

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/InnerProductSpace/Adjoint.html#ContinuousLinearMap.adjoint