Metamath Proof Explorer


Syntax definition cmulr

Description: Extend class notation with ring multiplication.

Ref Expression
Assertion cmulr class .r