Database
ELEMENTARY NUMBER THEORY
Elementary properties of divisibility
The least common multiple
clcmf
Next ⟩
df-lcm
Metamath Proof Explorer
Ascii
Unicode
Syntax definition
clcmf
Description:
Extend the definition of a class to include the least common multiple function.
Ref
Expression
Assertion
clcmf
class
lcm
_