7th-root-of-unity.egi

-- 7th root of unity

def z : MathExpr := rtu 7

def a11 : MathExpr := z ^ 1 + z ^ 6
def a12 : MathExpr := z ^ 2 + z ^ 5
def a13 : MathExpr := z ^ 3 + z ^ 4

def b10 : MathExpr := a11 + a12 + a13
def b10' : MathExpr := b10

assertEqual "b10'" b10' (-1)

def b11 : MathExpr := a11 + w * a12 + w ^ 2 * a13
def b12 : MathExpr := a13 + w * a11 + w ^ 2 * a12
def b13 : MathExpr := a12 + w * a13 + w ^ 2 * a11

def b11' : MathExpr := rt 3 (b11 * b12 * b13)

-- b11' = rt 3 (14 + 21 * w)

def b14 := a11 + w * a13 + w ^ 2 * a12
def b15 := a12 + w * a11 + w ^ 2 * a13
def b16 := a13 + w * a12 + w ^ 2 * a11

def b14' := rt 3 (b14 * b15 * b16)

-- b14' = rt 3 ((-7) + (-21) * w)

def a11' := (b10' + b11' + b14') / 3

def z1' := fst (qF' 1 (- a11') 1)

-- Expected result:
-- z1' = ((-1) + rt 3 (14 + 21 * w) + rt 3 ((-7) + (-21) * w) +
--        sqrt ((-35) + (-2) * rt 3 (14 + 21 * w) + (-2) * rt 3 ((-7) + (-21) * w) +
--              rt 3 (14 + 21 * w) ^ 2 + rt 3 ((-7) + (-21) * w) ^ 2 +
--              2 * rt 3 (14 + 21 * w) * rt 3 ((-7) + (-21) * w))) / 6