Metamath Proof Explorer


Syntax definition cplusg

Description: Extend class notation with group (addition) operation.

Ref Expression
Assertion cplusg
class +g