Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-30 06:52 04071ae3

View on Github →

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.

Estimated changes