Metamath Proof Explorer


Syntax definition cm1r

Description: The signed real constant -1.

Ref Expression
Assertion cm1r class -1R