Metamath Proof Explorer


Syntax definition cho

Description: Extend class notation with set of Hermitian Hilbert space operators.

Ref Expression
Assertion cho class HrmOp