def Hex.AlgebraicNumber.Radical.polynomial (a : AlgebraicNumber) (n : Nat) : AlgebraicPoly

The polynomial X^n - a, for the positive indices used by the root solver.

Equations

• Hex.AlgebraicNumber.Radical.polynomial a n = Hex.AlgebraicPoly.ofArray (Array.ofFn fun (i : Fin (n + 1)) => if ↑i = 0 then -a else if ↑i = n then 1 else 0)

def Hex.AlgebraicNumber.Radical.principalSide (a : AlgebraicNumber) : RootSide

The imaginary side containing the principal root for indices greater than one.

Equations

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

def Hex.AlgebraicNumber.Radical.fast? (a : AlgebraicNumber) (roots : Array RootCount) : Option AlgebraicRoot

Retain the principal half circle and certify its maximal real coordinate.

Equations

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

def Hex.AlgebraicNumber.nthRoot (a : AlgebraicNumber) (n : Nat) : AlgebraicNumber

The principal complex nth root, matching Complex.cpow with exponent 1/n. In particular nthRoot a 0 = 1, and the principal odd root of a negative real number need not be real. General inputs use the full polynomial root solver.

Equations

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

def Hex.AlgebraicNumber.sqrt (a : AlgebraicNumber) : AlgebraicNumber

The principal square root, with nonnegative real part and the positive imaginary branch on the negative real axis.

Equations

• a.sqrt = a.nthRoot 2

@[simp]

theorem Hex.AlgebraicNumber.nthRoot_zero (a : AlgebraicNumber) : a.nthRoot 0 = 1

@[simp]

theorem Hex.AlgebraicNumber.nthRoot_one (a : AlgebraicNumber) : a.nthRoot 1 = a