Metamath Proof Explorer


Syntax definition cfrgp

Description: Extend class notation with the free group construction.

Ref Expression
Assertion cfrgp class freeGrp