Documentation

CompPoly.Univariate.Roots.Backend

Finite-Field Root Backend #

Executable field-root extraction over finite fields. The public operation handles zero, constant, and linear cases explicitly, computes the finite-field root product modulo the input polynomial, splits the product into linear factors, then validates and deduplicates candidates against the original input.

source
def CompPoly.CPolynomial.Roots.FiniteField.rootsInFiniteFieldWith {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (M : Raw.MulContext F) (D : Raw.ModContext F) (ctx : FiniteFieldContext F) (splitter : LinearFactorProductSplitter F) (p : CPolynomial F) :
Array F

Executable roots of a univariate polynomial over a finite field.

Instances For
    source
    def CompPoly.CPolynomial.Roots.FiniteField.rootsInFiniteField {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (ctx : FiniteFieldContext F) (splitter : LinearFactorProductSplitter F) (p : CPolynomial F) :
    Array F

    Executable roots using the default raw multiplication and monic-remainder backends.

    Instances For