We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 6925c7e commit ab0cfbcCopy full SHA for ab0cfbc
Mathlib/Analysis/CStarAlgebra/Basic.lean
@@ -21,9 +21,8 @@ A C⋆-ring is a normed star group that is also a ring and that verifies the str
21
condition `‖x‖^2 ≤ ‖x⋆ * x‖` for all `x` (which actually implies equality). If a C⋆-ring is also
22
a star algebra, then it is a C⋆-algebra.
23
24
-To get a C⋆-algebra `E` over field `𝕜`, use
25
-`[NormedField 𝕜] [StarRing 𝕜] [NormedRing E] [StarRing E] [CStarRing E]
26
- [NormedAlgebra 𝕜 E] [StarModule 𝕜 E]`.
+Note that the type classes corresponding to C⋆-algebras are defined in
+`Mathlib/Analysis/CStarAlgebra/Classes`.
27
28
## TODO
29
0 commit comments