Metamath Proof Explorer

Syntax definition cmgp

Description: Multiplicative group.

Ref Expression
Assertion cmgp 
class mulGrp