spectral Spectral Theorem formalized in Coq, Draft! Use with caution Unfinished work. The use of forms is still very dirty for now... This is now a branch of mathcomp called forms, please do not depend on this repo anymore