Metamath Proof Explorer


Syntax definition cmp

Description: Positive real multiplication.

Ref Expression
Assertion cmp class ·P