Commit 2021-12-14 07:40 9af43e4e

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.