Metamath Proof Explorer


Syntax definition clcm

Description: Extend the definition of a class to include the least common multiple operator.

Ref Expression
Assertion clcm class lcm