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
1 Sakai’s Book
1.1
Definitions of \(C^{*}\)–algebras and \(W^{*}\)–algebras