17th Root of Unity

Calculating the 17th Root of Unity

On the 17th root of unity, the following equation is known.

`cos((2pi)/17) = 1/16(-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)))`.

We calucuate this value in the following code.
We utilize the fact that the Galois group of the following equation has same structure with the multiplicative group of `ZZ//17ZZ-{0}`.

`x^16 + x^15 + x^14 + x^13 + x^12 + x^11 + x^10 + x^9 + x^8 + x^7 + x^6 + x^5 + x^4 + x^3 + x^2 + x + 1 = 0` def z := rtu 17 def a1 := z ^ 1 + z ^ 16 def a2 := z ^ 2 + z ^ 15 def a3 := z ^ 3 + z ^ 14 def a4 := z ^ 4 + z ^ 13 def a5 := z ^ 5 + z ^ 12 def a6 := z ^ 6 + z ^ 11 def a7 := z ^ 7 + z ^ 10 def a8 := z ^ 8 + z ^ 9 def b11 := a1 + a4 def b12 := a1 - a4 def b21 := a2 + a8 def b22 := a2 - a8 def b31 := a3 + a5 def b32 := a3 - a5 def b41 := a6 + a7 def b42 := a6 - a7 def c11 := b11 + b21 def c12 := b11 - b21 def c21 := b31 + b41 def c22 := b31 - b41 def d10 := c11 + c21 def d11 := c11 - c21 def d12 := c21 - c11 def d10' := -1 def d11' := sqrt 17 def c11' := (d10' + d11') / 2 def c21' := (d10' - d11') / 2 def c12' := sqrt (8 + (- c11')) def c22' := sqrt (8 + (- c21')) def b11' := (c11' + c12') / 2 def b21' := (c11' - c12') / 2 def b31' := (c21' + c22') / 2 def b41' := (c21' - c22') / 2 def b12' := sqrt (4 + b21' + (-2) * b31') def b22' := sqrt (4 + b21' + (-2) * b41') def b32' := sqrt (4 + b41' + (-2) * b21') def b42' := sqrt (4 + b31' + (-2) * b21') def 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)

Links

Back to the Table of Contents