/usr/share/axiom-20170501/src/algebra/INTDOM.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 56 57 58 59 60 61 62 63 64 | )abbrev category INTDOM IntegralDomain
++ Description:
++ The category of commutative integral domains, commutative
++ rings with no zero divisors.
++
++ Conditional attributes\br
++ canonicalUnitNormal\tab{5}the canonical field is the same for
++ all associates\br
++ canonicalsClosed\tab{5}the product of two canonicals is itself canonical
IntegralDomain() : Category == SIG where
SIG ==> Join(CommutativeRing, Algebra(%), EntireRing) with
"exquo" : (%,%) -> Union(%,"failed")
++ exquo(a,b) either returns an element c such that
++ \spad{c*b=a} or "failed" if no such element can be found.
unitNormal : % -> Record(unit:%,canonical:%,associate:%)
++ unitNormal(x) tries to choose a canonical element
++ from the associate class of x.
++ The attribute canonicalUnitNormal, if asserted, means that
++ the "canonical" element is the same across all associates of x
++ if \spad{unitNormal(x) = [u,c,a]} then
++ \spad{u*c = x}, \spad{a*u = 1}.
unitCanonical : % -> %
++ \spad{unitCanonical(x)} returns \spad{unitNormal(x).canonical}.
associates? : (%,%) -> Boolean
++ associates?(x,y) tests whether x and y are associates,
++ differ by a unit factor.
unit? : % -> Boolean
++ unit?(x) tests whether x is a unit, is invertible.
add
x,y: %
UCA ==> Record(unit:%,canonical:%,associate:%)
if not (% has Field) then
unitNormal(x) == [1$%,x,1$%]$UCA -- the non-canonical definition
unitCanonical(x) == unitNormal(x).canonical -- always true
recip(x) == if zero? x then "failed" else _exquo(1$%,x)
unit?(x) == (recip x case "failed" => false; true)
if % has canonicalUnitNormal then
associates?(x,y) ==
(unitNormal x).canonical = (unitNormal y).canonical
else
associates?(x,y) ==
zero? x => zero? y
zero? y => false
x exquo y case "failed" => false
y exquo x case "failed" => false
true
|