mathlib

60ccf8f7 - feat(linear_algebra): add `adjoint_pair` from `bilinear_form` (#13203)

feat(linear_algebra): add `adjoint_pair` from `bilinear_form` (#13203) Copying the definition and theorem about adjoint pairs from `bilinear_form` to `sesquilinear_form`. Defines the composition of two linear maps with a bilinear map to form a new bilinear map, which was missing from the `bilinear_map` API. We also use the new definition of adjoint pairs in `analysis/inner_product_space/adjoint`.