Metamath Proof Explorer


Syntax definition cngp

Description: The class of all normed groups.

Ref Expression
Assertion cngp class NrmGrp