Operator Algebras in Lean
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
0.3 Products of nonnegative elements are nonnegative