Documentation

CompPoly.Univariate.Roots.Splitter

Linear-Factor Splitter Helpers #

Shared executable helpers for finite-field linear-factor splitters.

source
def CompPoly.CPolynomial.Roots.FiniteField.isRepresentedLinearFactor {F : Type u_1} [Field F] [BEq F] (p : CPolynomial F) :
Bool

Boolean recognizer for represented nonconstant linear factors.

Instances For
    source
    theorem CompPoly.CPolynomial.Roots.FiniteField.isRepresentedLinearFactor_sound {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] {p : CPolynomial F} (h : isRepresentedLinearFactor p = true) :
    IsLinearFactor p

    The represented-linear Boolean recognizer is sound.

    source
    def CompPoly.CPolynomial.Roots.FiniteField.representedLinearFactorArray {F : Type u_1} [Field F] [BEq F] (p : CPolynomial F) :
    Array (CPolynomial F)

    Return p as a singleton array if it is represented as a nonconstant linear factor.

    Instances For
      source
      def CompPoly.CPolynomial.Roots.FiniteField.xPowModWith {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (M : Raw.MulContext F) (D : Raw.ModContext F) (modulus : CPolynomial F) (exponent : ℕ) :
      CPolynomial F

      X^exponent mod modulus, lifted back to canonical polynomials.

      Instances For