continuous functional calculus

Stream: general

[Jireh Loreaux]

I'm pleased to announce that the continuous functional calculus is PR'ed as #17164 and is ready for review, modulo one last dependent PR. It's been a rather long time in coming. I plan to develop all the API for it after the port to Lean 4, but this is the key result.

[Scott Morrison]

This is awesome!