In the following link, you will find a library in Isabelle/HOL related to Hilbert spaces and bounded operators (work-in-progress). bounded-operators

@Jose Manuel Rodriguez Caballero Good to know.

Last updated: Sep 25 2022 at 22:23 UTC