Project idea: Continuous functional calculus for selfadjoint

Stream: LFTCM 2024

[Jireh Loreaux]

This should be an easy project. The goal is just to create an instance of docs#ContinuousFunctionalCalculus for p := IsSelfAdjoint, and A := Matrix n n 𝕜 where 𝕜 is ℝ or ℂ. Mathlib already has all the necessary pieces and they just need to be put together. After this, we could follow-up with the same instance for positive semidefinite matrices.