Commit 2021-11-12 20:02 6afda884

feat(analysis/inner_product_space/spectrum): diagonalization of self-adjoint endomorphisms (finite dimension) (#9995) Diagonalization of a self-adjoint endomorphism T of a finite-dimensional inner product space E over either ℝ or ℂ: construct a linear isometry T.diagonalization from E to the direct sum of T's eigenspaces, such that T conjugated by T.diagonalization is diagonal:

lemma diagonalization_apply_self_apply (v : E) (μ : eigenvalues T) :
  hT.diagonalization (T v) μ = (μ : 𝕜) • hT.diagonalization v μ