least common multiple fn (LeastCommonMultipleFn)

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

Ontologie

SUMO / NUMERIC-FUNCTIONS

Class(es)

třída

inheritable relation

funkce

relace s proměnným počtem argumentů
is instance of

least common multiple fn

Související termín(y)

assignment fn greatest common divisor fn list fn contrary attribute disjoint decomposition disjoint relation exhaustive attribute exhaustive decomposition holds partition

Axiomy (2)

jestliže "least common multiple fn()" se rovná number,
potom pro všechny element platí: jestliže element je a member of "()", potom "number mod element" se rovná

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

jestliže "least common multiple fn()" se rovná number,
potom neexistuje less tak, že less je menší než number a pro všechny element platí: jestliže element je a member of "()", potom "less mod element" se rovná

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