Database
COMPLEX TOPOLOGICAL VECTOR SPACES (DEPRECATED)
Operators on complex vector spaces
Definitions and basic properties
chmo
Next ⟩
df-aj
Metamath Proof Explorer
Ascii
Unicode
Syntax definition
chmo
Description:
Set of Hermitional (self-adjoint) operators.
Ref
Expression
Assertion
chmo
$${class}\mathrm{HmOp}$$