The continuous functional calculus in Lean

Anatole Dedecker, Jireh Loreaux

The continuous functional calculus is perhaps the most fundamental construction in the theory of operator algebras, especially $C^{\ast }$-algebras. Here we document our formalization…