0.1
Introduction
0.2
Continuous functional calculus
0.3
Products of nonnegative elements are nonnegative
1
Sakai’s Book
▶
1.1
Definitions of \(C^{*}\)–algebras and \(W^{*}\)–algebras
Dependency graph
Operator Algebras in Lean
Jireh Loreaux
0.1
Introduction
0.2
Continuous functional calculus
0.3
Products of nonnegative elements are nonnegative
1
Sakai’s Book
1.1
Definitions of \(C^{*}\)–algebras and \(W^{*}\)–algebras