Metamath Proof Explorer


Syntax definition cminusg

Description: Extend class notation with inverse of group element.

Ref Expression
Assertion cminusg
class invg