Commit 2022-08-16 04:11 5c91a35b

refactor(analysis/inner_product_space): rename is_self_adjoint to is_symmetric and add is_self_adjoint (#15326) We rename the current inner_product_space.is_self_adjoint to linear_map.is_symmetric (which states that inner (A x) y = inner x (A y) for all x,y : E) and add a new definition is_self_adjoint for has_star R. This definition is used to state theorems that were previously stated for linear_map.is_symmetric, but are actually about self-adjointness for continuous_linear_map. The Hellinger-Toeplitz theorem then becomes the construction of a self-adjoint operator from a symmetric operator, which is consistent with the functional analysis literature. Moreover, since the definitions are now in the correct namespaces, we can use dot-notation. Consequently, most parts of inner_product_space/rayleigh and inner_product_space/spectrum now use is_self_adjoint and are also now in the continuous_linear_map.is_self_adjoint namespace. For the finite-dimensional case we use is_symmetric, since continuity is not used anywhere. Finally, there are some minor cleanups in the matrix diagonalization file.