Metamath Proof Explorer


Syntax definition cplusg

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

Ref Expression
Assertion cplusg class +g