mathlib

9af43e4e - feat(analysis/inner_product_space/basic): inner product as a (continuous) sesquilinear map (#10684)

feat(analysis/inner_product_space/basic): inner product as a (continuous) sesquilinear map (#10684) This PR replaces `inner_right (v : E) : E →L[𝕜] 𝕜` (the inner product with a fixed left element as a continuous linear map) by `innerₛₗ : E →ₗ⋆[𝕜] E →ₗ[𝕜] 𝕜 ` and `innerSL : E →L⋆[𝕜] E →L[𝕜] 𝕜 `, which bundle the inner product as a sesquilinear map and as a continuous sesquilinear map respectively.