Metamath Proof Explorer - cmp

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Syntax Definition cmp 3782

Description: Positive real multiplication.

**Assertion**
Ref	Expression
cmp	class ·_P

See definition df-mp 3883 for more information.

Colors of variables: wff set class