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
65
66
67
68
69
70
71
72
73
74
75
76
|
<CD>
<CDName> algnums </CDName>
<CDURL> http://www.nag.co.uk/Projects/openmath/corecd/cd/algnums.ocd </CDURL>
<CDReviewDate> 2000-09-01 </CDReviewDate>
<CDDate> 1999-10-20 </CDDate>
<CDVersion> 1.01 </CDVersion>
<CDStatus> experimental </CDStatus>
<CDUses>
<CDName>nums</CDName>
<CDName>quant1</CDName>
<CDName>arith1</CDName>
<CDName>relation1</CDName>
</CDUses>
<Description>
Symbols defining algebraic numbers.
</Description>
<CDDefinition>
<Name> star </Name>
<Description>
Takes a single argument cyc which is a cyclotomic number.
If the cyclotomic cyc is an irrational element of a quadratic extension
of the rationals then star(cyc) is the unique Galois conjugate of
cyc that is different from cyc, otherwise star(cyc) is undefined.
</Description>
</CDDefinition>
<CDDefinition>
<Name> NthRootOfUnity </Name>
<Description>
This constructor function takes two positive integral arguments, n and r.
The value is e^{2*r*\pi*i/n}.
</Description>
<FMP>
<OMOBJ>
<OMBIND>
<OMS cd="quant1" name="forall"/>
<OMBVAR>
<OMV name="n"/>
<OMV name="r"/>
</OMBVAR>
<OMA>
<OMS cd="relation1" name="eq"/>
<OMA>
<OMS cd="algnums" name="NthRootOfUnity"/>
<OMV name="n"/>
<OMV name="r"/>
</OMA>
<OMA>
<OMS cd="arith1" name="power"/>
<OMS cd="nums" name="e"/>
<OMA>
<OMS cd="arith1" name="divide"/>
<OMA>
<OMS cd="arith1" name="times"/>
<OMI> 2 </OMI>
<OMS cd="nums" name="pi"/>
<OMS cd="nums" name="i"/>
<OMV name="r"/>
</OMA>
<OMV name="n"/>
</OMA>
</OMA>
</OMA>
</OMBIND>
</OMOBJ>
</FMP>
</CDDefinition>
</CD>
|
