17th-root-of-unity.egi

z := rtu 17

a1 := z ^ 1 + z ^ 16
a2 := z ^ 2 + z ^ 15
a3 := z ^ 3 + z ^ 14
a4 := z ^ 4 + z ^ 13
a5 := z ^ 5 + z ^ 12
a6 := z ^ 6 + z ^ 11
a7 := z ^ 7 + z ^ 10
a8 := z ^ 8 + z ^ 9

b11 := a1 + a4
b12 := a1 - a4

b21 := a2 + a8
b22 := a2 - a8

b31 := a3 + a5
b32 := a3 - a5

b41 := a6 + a7
b42 := a6 - a7

c11 := b11 + b21
c12 := b11 - b21

c21 := b31 + b41
c22 := b31 - b41

d10 := c11 + c21
d11 := c11 - c21
d12 := c21 - c11

d10' := -1

d11' := sqrt 17

c11' := (d10' + d11') / 2
c21' := (d10' - d11') / 2
c12' := sqrt (8 + (- c11'))
c22' := sqrt (8 + (- c21'))

b11' := (c11' + c12') / 2
b21' := (c11' - c12') / 2
b31' := (c21' + c22') / 2
b41' := (c21' - c22') / 2

b12' := sqrt (4 + b21' + (-2) * b31')
b22' := sqrt (4 + b21' + (-2) * b41')
b32' := sqrt (4 + b41' + (-2) * b21')
b42' := sqrt (4 + b31' + (-2) * b21')

a1' := (b11' + b12') / 2

assertEqual
  "17th-root-of-unity"
  a1'
  ((-1
    + sqrt 17
    + sqrt (34 + (-2) * sqrt 17)
    + 2 * sqrt (17 + 3 * sqrt 17 + (- sqrt (34 + (-2) * sqrt 17)) + (-2) * sqrt (34 + 2 * sqrt 17))) / 8)