)abbrev category ABELGRP AbelianGroup
++ Author:
++ Date Created:
++ Date Last Updated:
++ Basic Functions:
++ Related Constructors:
++ Also See:
++ AMS Classifications:
++ Keywords:
++ References:
++ Description:
++ The class of abelian groups, i.e. additive monoids where
++ each element has an additive inverse.
++
++ Axioms:
++ \spad{-(-x) = x}
++ \spad{x+(-x) = 0}
-- following domain must be compiled with subsumption disabled
AbelianGroup(): Category == Join(CancellationAbelianMonoid, LeftLinearSet Integer) with
-: % -> % ++ \spad{-x} is the additive inverse of \spad{x}
-: (%,%) -> % ++ \spad{x-y} is the difference of \spad{x}
++ and \spad{y} i.e. \spad{x + (-y)}.
add
(x:% - y:%):% == x+(-y)
subtractIfCan(x:%, y:%) == just(x-y)
n:NonNegativeInteger * x:% == (n::Integer) * x
import RepeatedDoubling(%)
if not (% has Ring) then
n:Integer * x:% ==
zero? n => 0
positive? n => double(n pretend PositiveInteger,x)
double((-n) pretend PositiveInteger,-x)
opposite?(x,y) == x = -y
