Commit 2021-12-24 16:32 3377bccd

feat(analysis/inner_product_space/adjoint): define the adjoint of a continuous linear map between Hilbert spaces (#10825) This PR defines the adjoint of an operator A : E →L[𝕜] F as the unique operator adjoint A : F →L[𝕜] E such that ⟪x, A y⟫ = ⟪adjoint A x, y⟫ for all x and y. We then use this to put a star algebra structure on E →L[𝕜] E with the adjoint as the star operation (while leaving the C* property for a subsequent PR).