Spectral theory of hermitian matrices #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
This file proves the spectral theorem for matrices. The proof of the spectral theorem is based on
the spectral theorem for linear maps (
spectral theorem, diagonalization theorem
The eigenvalues of a hermitian matrix, indexed by
fin (fintype.card n) where
n is the index
type of the matrix.
The eigenvalues of a hermitian matrix, reusing the index
n of the matrix entries.
A choice of an orthonormal basis of eigenvectors of a hermitian matrix.
A matrix whose columns are an orthonormal basis of eigenvectors of a hermitian matrix.
The inverse of
Diagonalization theorem, spectral theorem for matrices; A hermitian matrix can be
diagonalized by a change of basis.
For the spectral theorem on linear maps, see
The determinant of a hermitian matrix is the product of its eigenvalues.