Metamath Proof Explorer


Syntax definition cmp

Description: Positive real multiplication.

Ref Expression
Assertion cmp
class .P.