Commit 2021-11-15 04:19 62992fa9

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.