Metamath Proof Explorer


Syntax definition cnlm

Description: Normed module.

Ref Expression
Assertion cnlm class NrmMod