Metamath Proof Explorer


Syntax definition ctgrp

Description: Extend class notation with translation group.

Ref Expression
Assertion ctgrp class TGrp