Metamath Proof Explorer


Syntax definition cmg

Description: Extend class notation with a function mapping a group operation to the multiple/power operation for the magma/group.

Ref Expression
Assertion cmg class .g