29.9. Roots of unity🔗

Hex.AlgebraicNumber.rootOfUnity takes a rational number of full turns: rootOfUnity q means exp (2π I q). Negative angles and angles outside one turn are reduced modulo one. The reduced denominator is the exact order.

#guard AlgebraicNumber.rootOfUnity (1/4) == AlgebraicNumber.I
#guard AlgebraicNumber.rootOfUnity (-1/4) == -AlgebraicNumber.I
#guard AlgebraicNumber.rootOfUnity (7/6) == AlgebraicNumber.rootOfUnity (1/6)
example (q : Rat) : IsPrimitiveRoot (AlgebraicNumber.rootOfUnity q) q.den :=
  AlgebraicNumber.rootOfUnity_primitive q
example (q r : Rat) : AlgebraicNumber.rootOfUnity (q + r) =
    AlgebraicNumber.rootOfUnity q * AlgebraicNumber.rootOfUnity r :=
  AlgebraicNumber.rootOfUnity_add q r

Orders 1, 2, and 4 use constants. Other orders isolate an integer binomial: X^n - 1 for odd n, or X^(n/2) + 1 for even n. The upper root with greatest real part is the standard primitive generator. Selection uses lazy intervals, and subsequent powers are computed in its QAdjoin before one conversion back. This avoids the generic algebraic-coefficient solver, but polynomial degree still grows linearly with the denominator; large orders need the future cyclotomic algorithms.