Metamath Proof Explorer


Syntax definition cgi

Description: Extend class notation with a function mapping a group operation to the group's identity element.

Ref Expression
Assertion cgi
class GId