最小公倍數函數 (LeastCommonMultipleFn)

(LeastCommonMultipleFn number1 number2 ... number) returns the least common multiple of number1 through number.

Ontology

SUMO / NUMERIC-FUNCTIONS

Class(es)

種類

可繼承關係

函數

變異元數關係

最小公倍數函數

Coordinate term(s)

指定函數最大公約數函數序列函數矛盾屬性無交集分解無交集關係窮盡的屬性窮盡的分解成立分割

Axioms (2)

if " 的最小公倍數" 等於 number,
then for all element holds: if element 是 "()" 的一成員, then "number 取餘數 element" 等於

(=>
      (equal
            (LeastCommonMultipleFn @ROW)
            ?NUMBER)
      (forall
            (?ELEMENT)
            (=>
                  (inList
                        ?ELEMENT
                        (ListFn @ROW))
                  (equal
                        (RemainderFn ?NUMBER ?ELEMENT)
                        0))))

if " 的最小公倍數" 等於 number,
then there doesn't exist less so that less 小於 number and for all element holds: if element 是 "()" 的一成員, then "less 取餘數 element" 等於

(=>
      (equal
            (LeastCommonMultipleFn @ROW)
            ?NUMBER)
      (not
            (exists
                  (?LESS)
                  (and
                        (lessThan ?LESS ?NUMBER)
                        (forall
                              (?ELEMENT)
                              (=>
                                    (inList
                                          ?ELEMENT
                                          (ListFn @ROW))
                                    (equal
                                          (RemainderFn ?LESS ?ELEMENT)
                                          0)))))))