Metamath Proof Explorer

Syntax definition cmulr

Description: Extend class notation with ring multiplication.

Ref Expression
Assertion cmulr 
class .r