mathlib

04071ae3 - feat(analysis/inner_product_space/adjoint): define the adjoint for linear maps between finite-dimensional spaces (#11119)

feat(analysis/inner_product_space/adjoint): define the adjoint for linear maps between finite-dimensional spaces (#11119) This PR defines the adjoint of a linear map between finite-dimensional inner product spaces. We use the fact that such maps are always continuous and define it as the adjoint of the corresponding continuous linear map. Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>