Raw Univariate Polynomial Division

Division algorithms for raw computable univariate polynomials.

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

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

def CompPoly.CPolynomial.Raw.divModByMonicAux.go {R : Type u_1} [BEq R] [CommRing R] : ℕ → Raw R → Raw R → Raw R × Raw R

def CompPoly.CPolynomial.Raw.divByMonic {R : Type u_1} [BEq R] [CommRing R] (p q : Raw R) : Raw R

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

def CompPoly.CPolynomial.Raw.modByMonic {R : Type u_1} [BEq R] [CommRing R] (p q : Raw R) : Raw R

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

@[inline, specialize #[]]

def CompPoly.CPolynomial.Raw.subScaledShift {R : Type u_1} [BEq R] [Field R] (p q : Raw R) (scale : R) (shift : ℕ) : Raw R

Subtract scale * q * X^shift from p without using general polynomial multiplication.

@[inline, specialize #[]]

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

Remainder-only long division by a monic polynomial.

Unlike modByMonic, this does not compute the quotient and avoids the general polynomial multiplications used by each cancellation step. It is intended as an executable implementation for the canonical modByMonic specification.

def CompPoly.CPolynomial.Raw.modByMonicRemainderOnly.go {R : Type u_1} [BEq R] [Field R] : ℕ → Raw R → Raw R → Raw R

@[inline, specialize #[]]

def CompPoly.CPolynomial.Raw.inverseModX {R : Type u_1} [BEq R] [Field R] [LawfulBEq R] (M : MulLowContext R) (k : ℕ) (p : Raw R) : Raw R

Inverse modulo X^k, using Newton iteration and the supplied low-product backend.

def CompPoly.CPolynomial.Raw.inverseModX.go {R : Type u_1} [BEq R] [Field R] [LawfulBEq R] (M : MulLowContext R) (k : ℕ) (p : Raw R) : ℕ → ℕ → Raw R → Raw R

@[inline, specialize #[]]

def CompPoly.CPolynomial.Raw.modByMonicByReversal {R : Type u_1} [BEq R] [Field R] [LawfulBEq R] (M : MulLowContext R) (p q : Raw R) : Raw R

Remainder by a monic polynomial through reversal and truncated products.

For canonical monic inputs this computes the quotient from the reversed divisor inverse modulo X^k, then subtracts only the low coefficients needed for the remainder. Inputs outside the fast-path guard use the simple monic-remainder implementation.

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

Division of two CPolynomial.Raws.

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

Modulus of two CPolynomial.Raws.

@[implicit_reducible]

instance CompPoly.CPolynomial.Raw.instDivOfField {R : Type u_1} [BEq R] [Field R] : Div (Raw R)

@[implicit_reducible]

instance CompPoly.CPolynomial.Raw.instModOfField {R : Type u_1} [BEq R] [Field R] : Mod (Raw R)

def CompPoly.CPolynomial.Raw.monicNormalize {R : Type u_1} [BEq R] [Field R] (p : Raw R) : Raw R

Normalize a nonzero raw polynomial to monic form. The zero polynomial stays zero.

def CompPoly.CPolynomial.Raw.gcdMonicWithFuel {R : Type u_1} [BEq R] [Field R] : ℕ → Raw R → Raw R → Raw R

Raw Euclidean gcd with explicit fuel, normalized to a monic result.

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

Raw monic Euclidean gcd.