The least common multiple function can be called either with with an arbitrary number of integer arguments or with a single finite set of integers as the argument. The current entries only deal with the case of two arguments.
|
Table data:
such that
Definitions:
Fungrim symbol | Notation | Short description |
---|---|---|
LCM | Least common multiple | |
ZZ | Integers | |
ZZGreaterEqual | Integers greater than or equal to n | |
PowerSet | Power set | |
Cardinality | Set cardinality |
Source code for this entry:
Entry(ID("c03ed9"), SymbolDefinition(LCM, LCM(a, b), "Least common multiple"), Description("The least common multiple function can be called either with with an arbitrary number of integer arguments or with a single finite set of integers as the argument. The current entries only deal with the case of two arguments."), Table(TableRelation(Tuple(P, Q), Implies(P, Q)), TableHeadings(Description("Domain"), Description("Codomain")), List(Tuple(And(Element(a, ZZ), Element(b, ZZ)), Element(LCM(a, b), ZZGreaterEqual(0))), Tuple(And(Element(S, PowerSet(ZZ)), Less(Cardinality(S), Cardinality(ZZ))), Element(LCM(S), ZZGreaterEqual(0))))))