mathlib3

3377bccd - feat(analysis/inner_product_space/adjoint): define the adjoint of a continuous linear map between Hilbert spaces (#10825)

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). Co-authored-by: Heather Macbeth hmacbeth1@fordham.edu Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>