Documentation

CompPoly.Univariate.Raw.Division

Raw Univariate Polynomial Division #

Division algorithms for raw computable univariate polynomials.

source
def CompPoly.CPolynomial.Raw.divModByMonicAux {R : Type u_1} [BEq R] [Field R] (p q : Raw R) :
Raw R × Raw R

Division with remainder by a monic polynomial using polynomial long division.

Instances For
    source
    def CompPoly.CPolynomial.Raw.divModByMonicAux.go {R : Type u_1} [BEq R] [Field R] :
    ℕ → Raw R → Raw R → Raw R × Raw R
    Instances For
      source
      def CompPoly.CPolynomial.Raw.divByMonic {R : Type u_1} [BEq R] [Field R] (p q : Raw R) :
      Raw R

      Division of p : CPolynomial.Raw R by a monic q : CPolynomial.Raw R.

      Instances For
        source
        def CompPoly.CPolynomial.Raw.modByMonic {R : Type u_1} [BEq R] [Field R] (p q : Raw R) :
        Raw R

        Modulus of p : CPolynomial.Raw R by a monic q : CPolynomial.Raw R.

        Instances For
          source
          def CompPoly.CPolynomial.Raw.div {R : Type u_1} [BEq R] [Field R] (p q : Raw R) :
          Raw R

          Division of two CPolynomial.Raws.

          Instances For
            source
            def CompPoly.CPolynomial.Raw.mod {R : Type u_1} [BEq R] [Field R] (p q : Raw R) :
            Raw R

            Modulus of two CPolynomial.Raws.

            Instances For
              source
              @[implicit_reducible]
              instance CompPoly.CPolynomial.Raw.instDivOfField {R : Type u_1} [BEq R] [Field R] :
              Div (Raw R)
              source
              @[implicit_reducible]
              instance CompPoly.CPolynomial.Raw.instModOfField {R : Type u_1} [BEq R] [Field R] :
              Mod (Raw R)