Operator Algebras in Lean

Jireh Loreaux