Lean 4 - The Spectral Theorem
The principal assertion of the spectral theorem is that every bounded normal operator
This project
Current maintainers:
- Oliver Butterley
- Yoh Tanimoto
We aren't so wise to know for sure how big a task it will be to formalize this theorem but we believe we can make some good progress so we are trying. We also want to practice using the blueprint and github project way of collaborating as projects become larger.
See the project home page and Lean blueprint.
Collaborating
We welcome anyone who wants to be part of this.