Documentation

CompPoly.Bivariate.GuruswamiSudan.Root.FieldRoots

Guruswami-Sudan Field Roots #

Executable univariate field-root helpers used by Roth-Ruckenstein recursion. The explicit FieldRootContext context makes this dependency replaceable for large concrete fields.

source
def CompPoly.GuruswamiSudan.degreeLtBool {F : Type u_1} [Zero F] (p : CPolynomial F) (k : ℕ) :
Bool

Executable degree-< k check for canonical polynomials.

Instances For
    source
    @[reducible, inline]
    abbrev CompPoly.GuruswamiSudan.ContainsAllFieldElements {F : Type u_1} (elements : Array F) :
    Prop

    Compatibility alias for the univariate exhaustive-enumeration predicate.

    Instances For
      source
      def CompPoly.GuruswamiSudan.rootsInFieldByEnumeration {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (elements : Array F) (hElements : ContainsAllFieldElements elements) (p : CPolynomial F) :
      Array F

      Compatibility wrapper for roots by exhaustive evaluation over an explicit field list.

      Instances For
        source
        def CompPoly.GuruswamiSudan.enumeratingFieldRootContext (F : Type u_1) [Field F] [BEq F] [LawfulBEq F] (elements : Array F) (hElements : ContainsAllFieldElements elements) :
        FieldRootContext F

        Field roots by explicit enumeration over a supplied field-element list.

        Instances For