def Hex.DyadicSquare.meetsRealAxis (s : DyadicSquare) : Bool

The closed circumscribed disc, with its radius rounded up to radiusHi, meets the real axis.

Equations

• s.meetsRealAxis = (decide (-s.radiusHi ≤ s.im) && decide (s.im ≤ s.radiusHi))

def Hex.AlgebraicRoot.isReal (a : AlgebraicRoot) : Bool

The selected root is real. Exact at the stored separation precision.

Equations

• a.isReal = a.rep.val.square.meetsRealAxis

def Hex.AlgebraicNumber.isReal (a : AlgebraicNumber) : Bool

The represented number is real. Exact at the stored separation precision.

Equations

• a.isReal = a.rep.val.square.meetsRealAxis

def Hex.AlgebraicNumber.rootLe (a b : AlgebraicNumber) : Bool

The output order of ZPoly.algebraicRoots: real roots first, in increasing order of their isolation centres, which is their order as real numbers; then the nonreal roots ordered lexicographically by isolation centre, real part first, then imaginary part, then precision. That order is deterministic, but it depends on the isolations rather than on the roots alone, so no client should rely on more than its determinism.

Equations

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

def Hex.AlgebraicNumber.approx (a : AlgebraicNumber) (prec : Int := 64) : DyadicComplexBall

A dyadic complex ball of radius at most 2^(-prec) around the value, evaluated on the stored representative.

Equations

• a.approx prec = (Hex.PolyQuot.approx a.toQAdjoin a.rep ⋯ prec).snd

def Hex.AlgebraicRoot.ofRefined (q : ZPoly) (prim : q.content = 1) (pos_lc : 0 < DensePoly.leadingCoeff q) (pos_degree : 0 < DensePoly.natDegree q) (squarefree : HasOnlySimpleRoots q) (rep : RefinedIsolation q) : AlgebraicRoot

The lazy root selected by one refined isolation of a normalized squarefree polynomial.

Equations

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

@[irreducible]

def Hex.ZPoly.algebraicRoots? (p : ZPoly) : Option (Array AlgebraicNumber)

Every distinct complex root of p as a canonical algebraic number, or none if a certificate could not be produced. See algebraicRoots.

Irreducible, like algebraicRoots, so that a type such as PolyQuot a.p a.x for a root a found here is cheap to reduce: #eval reduces the type of a value while looking for a printing instance, and must not run the root isolation symbolically. Proofs unfold it explicitly.

Equations

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

@[irreducible]

def Hex.ZPoly.algebraicRoots (p : ZPoly) : Array AlgebraicNumber

Every distinct complex root of p as a canonical algebraic number: the squarefree primitive part of p is isolated, and each isolated root is exactified. Real roots come first, in increasing order, then the nonreal roots in a deterministic order set by their isolations. Multiplicities are not returned; use AlgebraicPoly.roots for them. A constant polynomial, including zero, has no roots here. Irreducible for the reason given at algebraicRoots?.

Equations

• p.algebraicRoots = p.algebraicRoots?.getD (Hex.panicWith #[] "ZPoly.algebraicRoots: certification failed")

def Hex.Display.dyadic : Dyadic → String

A dyadic as the expression that rebuilds it. Dyadic is a core inductive with no Repr; ofOdd n k denotes n · 2⁻ᵏ, which is ofIntWithPrec n k.

Equations

• One or more equations did not get rendered due to their size.
• Hex.Display.dyadic Dyadic.zero = "0"

def Hex.Display.square (s : DyadicSquare) : String

A square as the anonymous constructor its three fields rebuild.

Equations

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

@[instance_reducible]

unsafe instance Hex.instReprPolyQuot {p : ZPoly} {x : SimpleRoot p} : Repr (PolyQuot p x)

A fixed-field element prints as the expression that rebuilds it: its reduced coordinates ascribed to the presentation they live in, with the root named by the square that isolates it (SimpleRoot.ofSquare, whose two side conditions are decide-discharged auto-parameters).

The representative comes out of the Quot by unquot, as Mathlib's Multiset and Finset instances do, so the instance is unsafe and the printed square is whichever representative the value happens to carry. That choice is invisible in the result: Intersects compares stored squares, so every representative of the root rebuilds the same element.

Equations

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