Metamath Proof Explorer


Syntax definition ccring

Description: Extend class notation with the class of commutative rings.

Ref Expression
Assertion ccring class CRingOps