Metamath Proof Explorer


Syntax definition cmi

Description: Positive integer multiplication.

Ref Expression
Assertion cmi class ·N