The greatest common divisor 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 |
---|---|---|
GCD | Greatest common divisor | |
ZZ | Integers | |
ZZGreaterEqual | Integers greater than or equal to n | |
PowerSet | Power set | |
Cardinality | Set cardinality |
Source code for this entry:
Entry(ID("287e28"), SymbolDefinition(GCD, GCD(a, b), "Greatest common divisor"), Description("The greatest common divisor 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(GCD(a, b), ZZGreaterEqual(0))), Tuple(And(Element(S, PowerSet(ZZ)), Less(Cardinality(S), Cardinality(ZZ))), Element(GCD(S), ZZGreaterEqual(0))))))