leanprover-community / mathlib

  • Home
  • Zulip archive
  • API documentation
  • Lean web editor
  • Links

Zulip Chat Archive

Stream: general

Topic: continuous functional calculus


Jireh Loreaux (Nov 13 2022 at 08:11):

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 (Nov 13 2022 at 08:43):

This is awesome!


Last updated: May 02 2025 at 03:31 UTC

Theme Simple by wildflame © 2016 Powered by jekyll