def Hex.AlgebraicPolyNormalized (coeffs : Array AlgebraicNumber) : Prop

A coefficient array has no trailing semantic zero. This erased invariant is carried by AlgebraicPoly so downstream correctness theorems may quantify over every value, rather than only values visibly built by ofArray.

Equations

• Hex.AlgebraicPolyNormalized coeffs = match coeffs.toList.reverse.head? with | some a => a.isZero = false | none => True

structure Hex.AlgebraicPoly : Type

A semantically normalized polynomial with canonical algebraic coefficients. Construction is sealed so every stored array has had its trailing semantic zeros removed.

• data : Array AlgebraicNumber

  The stored coefficients, in increasing degree order.

• normalized : AlgebraicPolyNormalized self.data

  The stored coefficients have no trailing semantic zero.

def Hex.AlgebraicPoly.ofArray (coeffs : Array AlgebraicNumber) : AlgebraicPoly

Construct a polynomial and remove all trailing coefficients whose canonical minimal polynomial is X.

Equations

• Hex.AlgebraicPoly.ofArray coeffs = { data := Array.popWhile (fun (a : Hex.AlgebraicNumber) => a.isZero) coeffs, normalized := ⋯ }

def Hex.AlgebraicPoly.coeffs (f : AlgebraicPoly) : Array AlgebraicNumber

The normalized coefficient array, in increasing degree order.

Equations

• f.coeffs = f.data

def Hex.AlgebraicPoly.size (f : AlgebraicPoly) : Nat

Number of stored coefficients.

Equations

• f.size = f.data.size

def Hex.AlgebraicPoly.coeff (f : AlgebraicPoly) (n : Nat) : AlgebraicNumber

Coefficient at degree n, defaulting to canonical zero.

Equations

• f.coeff n = f.data.getD n 0

def Hex.AlgebraicPoly.isZero (f : AlgebraicPoly) : Bool

Semantic zero test.

Equations

• f.isZero = f.data.isEmpty

def Hex.AlgebraicPoly.degree? (f : AlgebraicPoly) : Option Nat

Degree of a nonzero polynomial.

Equations

• f.degree? = if f.isZero = true then none else some (f.size - 1)

@[reducible, inline]

abbrev Hex.AlgebraicPoly.natDegree (f : AlgebraicPoly) : Nat

The degree, with the zero polynomial given degree 0, matching DensePoly.natDegree.

Equations

• f.natDegree = f.degree?.getD 0

def Hex.AlgebraicPoly.beq (f g : AlgebraicPoly) : Bool

Canonical coefficientwise Boolean equality.

Equations

• f.beq g = (f.data == g.data)

@[instance_reducible]

instance Hex.AlgebraicPoly.instBEq : BEq AlgebraicPoly

Equations

• Hex.AlgebraicPoly.instBEq = { beq := Hex.AlgebraicPoly.beq }