integer1 http://www.openmath.org/cd/integer1.ocd 2003-04-01 2001-03-12 2 0 official logic1 quant1 set1 arith1 setname1 relation1 fns1 alg1 interval1 This CD holds a collection of basic integer functions. This CD is intended to be `compatible' with the corresponding elements in Content MathML. factorof This is the binary OpenMath operator that is used to indicate the mathematical relationship a "is a factor of" b, where a is the first argument and b is the second. This relationship is true if and only if b mod a = 0. b is a factor of a iff remainder of a divided by b = 0 factorial The symbol to represent a unary factorial function on non-negative integers. factorial n = product [1..n] 1 quotient The symbol to represent the integer (binary) division operator. That is, for integers a and b, quotient(a,b) denotes q such that a=b*q+r, with |r| less than |b| and a*r positive. for all a,b with a,b Integers | a = b * quotient(a,b) + remainder(a,b) and abs(remainder(a,b)) is less than abs(b) and a*remainder(a,b) >= 0 remainder The symbol to represent the integer remainder after (binary) division. For integers a and b, remainder(a,b) denotes r such that a=b*q+r, with |r| less than |b| and a*r positive. for all a,b with a,b Integers | a = b * quotient(a,b) + remainder(a,b) and abs(remainder(a,b)) is less than abs(b) and a*remainder(a,b) >= 0