/usr/share/axiom-20170501/src/algebra/FIELD.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 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 | )abbrev category FIELD Field
++ Description:
++ The category of commutative fields, commutative rings
++ where all non-zero elements have multiplicative inverses.
++ The \spadfun{factor} operation while trivial is useful to have defined.
++
++ Axioms\br
++ \tab{5}\spad{a*(b/a) = b}\br
++ \tab{5}\spad{inv(a) = 1/a}
Field() : Category == SIG where
SIG ==> Join(EuclideanDomain,UniqueFactorizationDomain,DivisionRing) with
"/" : (%,%) -> %
++ x/y divides the element x by the element y.
++ Error: if y is 0.
canonicalUnitNormal
++ either 0 or 1.
canonicalsClosed
++ since \spad{0*0=0}, \spad{1*1=1}
add
x,y: %
n: Integer
UCA ==> Record(unit:%,canonical:%,associate:%)
unitNormal(x) ==
if zero? x then [1$%,0$%,1$%]$UCA else [x,1$%,inv(x)]$UCA
unitCanonical(x) == if zero? x then x else 1
associates?(x,y) == if zero? x then zero? y else not(zero? y)
inv x ==((u:=recip x) case "failed" => error "not invertible"; u)
x exquo y == (y=0 => "failed"; x / y)
gcd(x,y) == 1
euclideanSize(x) == 0
prime? x == false
squareFree x == x::Factored(%)
factor x == x::Factored(%)
x / y == (zero? y => error "catdef: division by zero"; x * inv(y))
divide(x,y) == [x / y,0]
|