mathlib

62992fa9 - feat(analysis/inner_product_space/spectrum): more concrete diagonalization theorem (#10317)

feat(analysis/inner_product_space/spectrum): more concrete diagonalization theorem (#10317) This is a second version of the diagonalization theorem for self-adjoint operators on finite-dimensional inner product spaces, stating that a self-adjoint operator admits an orthonormal basis of eigenvectors, and deducing the standard consequences (when expressed with respect to this basis the operator acts diagonally). I have also updated `undergrad.yaml` and `overview.yaml` to cover the diagonalization theorem and other things proved in the library about Hilbert spaces.