mathlib3

6afda884 - feat(analysis/inner_product_space/spectrum): diagonalization of self-adjoint endomorphisms (finite dimension) (#9995)

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: ```lean lemma diagonalization_apply_self_apply (v : E) (μ : eigenvalues T) : hT.diagonalization (T v) μ = (μ : 𝕜) • hT.diagonalization v μ ``` Co-authored-by: Frédéric Dupuis <dupuisf@iro.umontreal.ca>