Documentation

CompPoly.Univariate.Raw.Modular

Raw Modular Operations on Univariate Polynomials #

Context-parametric modular multiplication and exponentiation over raw univariate polynomials.

source
def CompPoly.CPolynomial.Raw.mulModWith {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (M : MulContext F) (D : ModContext F) (modulus p q : Raw F) :
Raw F

Raw multiplication modulo a polynomial, treating zero modulus as no reduction.

Instances For
    source
    @[irreducible]
    def CompPoly.CPolynomial.Raw.powModBinaryAuxWith {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (M : MulContext F) (D : ModContext F) (modulus : Raw F) :
    ℕ → Raw F → Raw F → Raw F

    Raw binary modular exponentiation accumulator.

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

      Raw modular exponentiation by repeated squaring.

      Instances For
        source
        def CompPoly.CPolynomial.Raw.xModWith {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (D : ModContext F) :
        Raw F → Raw F

        Raw X mod modulus, with zero modulus treated as no reduction.

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

          Raw (X^q mod modulus) - (X mod modulus), without materializing X^q - X.

          Instances For