∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →ₗ[𝕜] E} [inst_3 : FiniteDimensional 𝕜 E] (hT : T.IsSymmetric) (v : E) (μ : Module.End.Eigenvalues T),
  (hT.diagonalization (T v)).ofLp μ = ↑T 1 μ • (hT.diagonalization v).ofLp μ