/usr/share/axiom-20170501/src/algebra/ABELGRP.spad is in axiom-source 20170501-3.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 | )abbrev category ABELGRP AbelianGroup
++ Description:
++ The class of abelian groups, additive monoids where
++ each element has an additive inverse.
++
++ Axioms\br
++ \tab{5}\spad{-(-x) = x}\br
++ \tab{5}\spad{x+(-x) = 0}
-- following domain must be compiled with subsumption disabled
AbelianGroup() : Category == SIG where
SIG ==> CancellationAbelianMonoid with
"-" : % -> %
++ -x is the additive inverse of x.
"-" : (%,%) -> %
++ x-y is the difference of x and y \spad{x + (-y)}.
-- subsumes the partial subtraction from previous
"*" : (Integer,%) -> %
++ n*x is the product of x by the integer n.
add
(x:% - y:%):% == x+(-y)
subtractIfCan(x:%, y:%):Union(%, "failed") == (x-y)::Union(%,"failed")
n:NonNegativeInteger * x:% == (n::Integer) * x
import RepeatedDoubling(%)
if not (% has Ring) then
n:Integer * x:% ==
zero? n => 0
n>0 => double(n pretend PositiveInteger,x)
double((-n) pretend PositiveInteger,-x)
|