Metamath Proof Explorer


Syntax definition cmq

Description: Positive fraction multiplication.

Ref Expression
Assertion cmq class ·Q