Metamath Proof Explorer


Syntax definition clcmf

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

Ref Expression
Assertion clcmf class lcm _