def Hex.QAdjoin.powerTable (a : AlgebraicNumber) : Array AlgebraicNumber

Consecutive powers used by coordinate recovery. Certification cannot fail.

Equations

• Hex.QAdjoin.powerTable a = (Hex.AlgebraicPoly.Common.powers? a (2 * Hex.DensePoly.natDegree a.p - 2)).getD (Hex.panicWith #[] "QAdjoin: power table certification failed")

def Hex.QAdjoin.ofAlgebraic? (a b : AlgebraicNumber) : Option (QAdjoin a)

Express b in the power basis of a, or return none when b ∉ ℚ(a). This does not enlarge the chosen field. A real generator rejects nonreal values before coordinate recovery.

Equations

• Hex.QAdjoin.ofAlgebraic? a b = if (a.isReal && !b.isReal) = true then none else Hex.AlgebraicPoly.Common.coordinates? a b (Hex.QAdjoin.powerTable a)

def Hex.QAdjoin.ofAlgebraics? (a : AlgebraicNumber) (bs : Array AlgebraicNumber) : Array (Option (QAdjoin a))

Convert a collection to one chosen field, sharing its power table. The output preserves input order and records nonmembership separately for each entry.

Equations

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

structure Hex.QAdjoin.Presentation : Type

One primitive generator and the input values in its rational power basis. The public entries name describes arbitrary input collections independently of AlgebraicPoly.Common.Presentation, whose coefficients field serves polynomial construction.

• generator : AlgebraicNumber
• entries : Array (QAdjoin self.generator)

def Hex.QAdjoin.common (bs : Array AlgebraicNumber) : Presentation

Find one number field containing every input, preserving order and duplicates. Empty and all-zero collections use ℚ(0) = ℚ. The primitive-element search can be expensive; subsequent arithmetic in the resulting QAdjoin uses rational coordinates without further root isolation.

Equations

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