instance Hex.AlgebraicNumber.instCheckedIrreducibleP (a : AlgebraicNumber) : a.p.CheckedIrreducible

The minimal polynomial of a canonical algebraic number carries checked irreducibility, so PolyQuot a.p a.x has inversion and division without the evidence being registered by hand.

@[implicit_reducible]

def Hex.QAdjoin (a : AlgebraicNumber) : Type

The fixed field ℚ(a) of a canonical algebraic number: the presentation ring on its minimal polynomial, with the embedding fixed by the root it denotes. Reducible, so every PolyQuot operation, instance and theorem applies unchanged.

Equations

• Hex.QAdjoin a = Hex.PolyQuot a.p a.x

@[instance_reducible]

instance Hex.instDecidableEqQAdjoin {a : AlgebraicNumber} : DecidableEq (QAdjoin a)

Equations

• Hex.instDecidableEqQAdjoin = Hex.instDecidableEqQAdjoin._aux_1

@[instance_reducible]

instance Hex.instZeroQAdjoin {a : AlgebraicNumber} : Zero (QAdjoin a)

Equations

• Hex.instZeroQAdjoin = { zero := Hex.instZeroQAdjoin._aux_1 }

@[instance_reducible]

instance Hex.instOneQAdjoin {a : AlgebraicNumber} : One (QAdjoin a)

Equations

• Hex.instOneQAdjoin = { one := Hex.instOneQAdjoin._aux_1 }

@[instance_reducible]

instance Hex.instAddQAdjoin {a : AlgebraicNumber} : Add (QAdjoin a)

Equations

• Hex.instAddQAdjoin = { add := Hex.instAddQAdjoin._aux_1 }

@[instance_reducible]

instance Hex.instSubQAdjoin {a : AlgebraicNumber} : Sub (QAdjoin a)

Equations

• Hex.instSubQAdjoin = { sub := Hex.instSubQAdjoin._aux_1 }

@[instance_reducible]

instance Hex.instNegQAdjoin {a : AlgebraicNumber} : Neg (QAdjoin a)

Equations

• Hex.instNegQAdjoin = { neg := Hex.instNegQAdjoin._aux_1 }

@[instance_reducible]

instance Hex.instMulQAdjoin {a : AlgebraicNumber} : Mul (QAdjoin a)

Equations

• Hex.instMulQAdjoin = { mul := Hex.instMulQAdjoin._aux_1 }

@[instance_reducible]

instance Hex.instSMulRatQAdjoin {a : AlgebraicNumber} : SMul Rat (QAdjoin a)

Equations

• Hex.instSMulRatQAdjoin = { smul := Hex.instSMulRatQAdjoin._aux_1 }

@[instance_reducible]

instance Hex.instCoeDensePolyRatQAdjoin {a : AlgebraicNumber} : Coe (DensePoly Rat) (QAdjoin a)

Equations

• Hex.instCoeDensePolyRatQAdjoin = { coe := Hex.instCoeDensePolyRatQAdjoin._aux_1 }

@[instance_reducible]

instance Hex.instNatCastQAdjoin {a : AlgebraicNumber} : NatCast (QAdjoin a)

Equations

• Hex.instNatCastQAdjoin = { natCast := Hex.instNatCastQAdjoin._aux_1 }

@[instance_reducible]

instance Hex.instIntCastQAdjoin {a : AlgebraicNumber} : IntCast (QAdjoin a)

Equations

• Hex.instIntCastQAdjoin = { intCast := Hex.instIntCastQAdjoin._aux_1 }

@[instance_reducible, instance 90]

instance Hex.instOfNatQAdjoinHAddNatOfNat {a : AlgebraicNumber} (n : Nat) : OfNat (QAdjoin a) (n + 2)

Equations

• Hex.instOfNatQAdjoinHAddNatOfNat n = { ofNat := Hex.instOfNatQAdjoinHAddNatOfNat._aux_1 n }

@[instance_reducible]

instance Hex.instInvQAdjoin {a : AlgebraicNumber} : Inv (QAdjoin a)

Equations

• Hex.instInvQAdjoin = { inv := Hex.instInvQAdjoin._aux_1 }

@[instance_reducible]

instance Hex.instDivQAdjoin {a : AlgebraicNumber} : Div (QAdjoin a)

Equations

• Hex.instDivQAdjoin = { div := Hex.instDivQAdjoin._aux_1 }

@[instance_reducible]

instance Hex.instPowQAdjoinNat {a : AlgebraicNumber} : Pow (QAdjoin a) Nat

Equations

• Hex.instPowQAdjoinNat = { pow := Hex.instPowQAdjoinNat._aux_1 }

@[instance_reducible]

instance Hex.instPowQAdjoinInt {a : AlgebraicNumber} : Pow (QAdjoin a) Int

Equations

• Hex.instPowQAdjoinInt = { pow := Hex.instPowQAdjoinInt._aux_1 }

def Hex.QAdjoin.ofCoeffs (a : AlgebraicNumber) (f : DensePoly Rat) : QAdjoin a

The element of ℚ(a) with coordinates f in the power basis of a. Unlike PolyQuot.ofSquare this needs no square and no side conditions: the generating number already carries its own root.

Equations

• Hex.QAdjoin.ofCoeffs a f = Hex.PolyQuot.reduce a.p a.x f

def Hex.AlgebraicNumber.toQAdjoin (a : AlgebraicNumber) : QAdjoin a

The canonical algebraic number as the generator of its own fixed field.

Equations

• a.toQAdjoin = Hex.PolyQuot.reduce a.p a.x (Hex.DensePoly.ofList [0, 1])

def Hex.AlgebraicNumber.toRoot (a : AlgebraicNumber) : AlgebraicRoot

Forget minimality while retaining every checked root certificate.

Equations

• a.toRoot = { p := a.p, prim := ⋯, pos_lc := ⋯, pos_degree := ⋯, squarefree := ⋯, x := a.x, rep := a.rep, rep_mk := ⋯ }

def Hex.AlgebraicRoot.exactFactor? (a : AlgebraicRoot) (q : ZPoly) : Option AlgebraicNumber

Try one normalized factor of a lazy root's enclosing polynomial. Candidate isolations are refined to the enclosing polynomial's separation precision before their discs are compared.

Equations

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

def Hex.AlgebraicRoot.exact? (a : AlgebraicRoot) : Option AlgebraicNumber

Factor a lazy root's enclosing polynomial and select the normalized irreducible factor containing its chosen root. none is a checked implementation branch whose unreachability is proved by the Mathlib companion.

Equations

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

def Hex.AlgebraicRoot.exact (a : AlgebraicRoot) : AlgebraicNumber

Canonicalize a lazy root: the total form of exact?, whose none branch the Mathlib companion proves unreachable.

Equations

• a.exact = a.exact?.getD (Hex.panicWith 0 "AlgebraicRoot.exact: certification failed")

def Hex.PolyQuot.krylovPowers {p : ZPoly} {x : SimpleRoot p} (a : PolyQuot p x) (n : Nat) : Vector (PolyQuot p x) (n + 1)

The first n + 1 Krylov powers, built with one multiplication per step.

Equations

• a.krylovPowers 0 = #v[1]
• a.krylovPowers n.succ = (a.krylovPowers n).push ((a.krylovPowers n).get (Fin.last n) * a)

def Hex.PolyQuot.krylovOrbit {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (a : PolyQuot p x) : Vector (PolyQuot p x) (DensePoly.natDegree p + 1)

Krylov orbit 1, a, a², ... through the defining-field dimension.

Equations

• a.krylovOrbit = a.krylovPowers (Hex.DensePoly.natDegree p)

def Hex.PolyQuot.relationPoly {k : Nat} (coeffs : Vector Rat k) : DensePoly Rat

The monic polynomial encoded by a Krylov dependence vector.

Equations

• Hex.PolyQuot.relationPoly coeffs = Hex.DensePoly.ofCoeffs ((Array.map (fun (c : Rat) => -c) coeffs.toArray).push 1)

def Hex.PolyQuot.relationAt? {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (_a : PolyQuot p x) (orbit : Vector (PolyQuot p x) (DensePoly.natDegree p + 1)) (k : Nat) : Option ZPoly

The monic relation at one Krylov-orbit index, when the new power is in the span of its predecessors.

Equations

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

def Hex.PolyQuot.minpoly? {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (a : PolyQuot p x) : Option ZPoly

First monic relation in the Krylov orbit of the multiplication operator, normalized as a primitive positive-leading integer polynomial.

Equations

• a.minpoly? = List.findSome? (fun (i : Nat) => a.relationAt? a.krylovOrbit (i + 1)) (List.range (Hex.DensePoly.natDegree p))

def Hex.PolyQuot.toAlgebraicNumber? {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (a : PolyQuot p x) (rep : RefinedIsolation p) (_h : SimpleRoot.mk rep = x) : Option AlgebraicNumber

Convert a fixed-presentation value to its canonical irreducible representation. Every stored certificate and every precision-sensitive step is checked before construction.

Equations

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

def Hex.PolyQuot.toAlgebraicNumber {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (a : PolyQuot p x) (rep : RefinedIsolation p) (h : SimpleRoot.mk rep = x) : AlgebraicNumber

Total fixed-presentation conversion. The checked failure branch is proved unreachable by the Mathlib companion.

Equations

• a.toAlgebraicNumber rep h = (a.toAlgebraicNumber? rep h).getD (Hex.panicWith 0 "PolyQuot.toAlgebraicNumber: certification failed")

def Hex.QAdjoin.toAlgebraicNumber? {a : AlgebraicNumber} (c : QAdjoin a) : Option AlgebraicNumber

The canonical number an element of ℚ(a) denotes, or none if the certification failed. The general form applied with a's own representative.

Equations

• c.toAlgebraicNumber? = Hex.PolyQuot.toAlgebraicNumber? c a.rep ⋯

def Hex.QAdjoin.toAlgebraicNumber {a : AlgebraicNumber} (c : QAdjoin a) : AlgebraicNumber

The canonical number an element of ℚ(a) denotes.

Equations

• c.toAlgebraicNumber = Hex.PolyQuot.toAlgebraicNumber c a.rep ⋯