def Hex.AlgebraicNumber.Unity.polynomial (n : Nat) : ZPoly

For even orders, the smaller binomial already contains the primitive root.

Equations

• Hex.AlgebraicNumber.Unity.polynomial n = if n % 2 = 0 then Hex.DensePoly.monomial (n / 2) 1 + Hex.DensePoly.C 1 else Hex.DensePoly.monomial n 1 - Hex.DensePoly.C 1

def Hex.AlgebraicNumber.Unity.generator? (n : Nat) : Option AlgebraicNumber

Select the upper root nearest to the positive real axis.

Equations

• One or more equations did not get rendered due to their size.

def Hex.AlgebraicNumber.Unity.generator (n : Nat) : AlgebraicNumber

The standard positive primitive nth root; order zero is defined as one.

Equations

• Hex.AlgebraicNumber.Unity.generator n = match Hex.AlgebraicNumber.Unity.generator? n with | some a => a | none => Hex.panicWith 1 "AlgebraicNumber.rootOfUnity: root selection failed"

def Hex.AlgebraicNumber.Unity.power (a : AlgebraicNumber) (k : Nat) : AlgebraicNumber

Power in a single presentation, exactifying once at the end.

Equations

• Hex.AlgebraicNumber.Unity.power a k = (a.toQAdjoin ^ k).toAlgebraicNumber

def Hex.AlgebraicNumber.rootOfUnity (q : Rat) : AlgebraicNumber

The root of unity exp (2*pi*I*q). The rational angle is reduced modulo one; its reduced denominator is the exact order. General orders isolate an integer binomial, select one primitive generator, and use fixed-field powers.

Equations

• One or more equations did not get rendered due to their size.