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.

Equations

• p.divModByMonicAux q = CompPoly.CPolynomial.Raw.divModByMonicAux.go (Array.size p) p q

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

Equations

• One or more equations did not get rendered due to their size.
• CompPoly.CPolynomial.Raw.divModByMonicAux.go 0 a✝¹ a✝ = (0, a✝¹)

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.

Equations

• p.divByMonic q = (p.divModByMonicAux q).1

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.

Equations

• p.modByMonic q = (p.divModByMonicAux q).2

@[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.

Equations

• One or more equations did not get rendered due to their size.

@[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.

Equations

• p.modByMonicRemainderOnly q = CompPoly.CPolynomial.Raw.modByMonicRemainderOnly.go (Array.size p) p q

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

Equations

• One or more equations did not get rendered due to their size.
• CompPoly.CPolynomial.Raw.modByMonicRemainderOnly.go 0 a✝¹ a✝ = a✝¹

@[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.

Equations

• CompPoly.CPolynomial.Raw.inverseModX M k p = if k = 0 then #[] else CompPoly.CPolynomial.Raw.inverseModX.go M k p (k + 1) 1 (CompPoly.CPolynomial.Raw.C (p.coeff 0)⁻¹)

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

Equations

• One or more equations did not get rendered due to their size.
• CompPoly.CPolynomial.Raw.inverseModX.go M k p 0 a✝¹ a✝ = CompPoly.CPolynomial.Raw.truncate k a✝

@[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.

Equations

• One or more equations did not get rendered due to their size.

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

Division of two CPolynomial.Raws.

Equations

• p.div q = (CompPoly.CPolynomial.Raw.C q.leadingCoeff⁻¹ • p).divByMonic (CompPoly.CPolynomial.Raw.C q.leadingCoeff⁻¹ * q)

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

Modulus of two CPolynomial.Raws.

Equations

• p.mod q = (CompPoly.CPolynomial.Raw.C q.leadingCoeff⁻¹ • p).modByMonic (CompPoly.CPolynomial.Raw.C q.leadingCoeff⁻¹ * q)

@[instance_reducible]

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

Equations

• CompPoly.CPolynomial.Raw.instDivOfField = { div := CompPoly.CPolynomial.Raw.div }

@[instance_reducible]

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

Equations

• CompPoly.CPolynomial.Raw.instModOfField = { mod := CompPoly.CPolynomial.Raw.mod }

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.

Equations

• p.monicNormalize = if (p.trim == 0) = true then 0 else p.trim.leadingCoeff⁻¹ • p.trim

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.

Equations

• CompPoly.CPolynomial.Raw.gcdMonicWithFuel 0 x✝¹ x✝ = x✝¹.monicNormalize
• CompPoly.CPolynomial.Raw.gcdMonicWithFuel n.succ x✝¹ x✝ = if (x✝.trim == 0) = true then x✝¹.trim.monicNormalize else CompPoly.CPolynomial.Raw.gcdMonicWithFuel n x✝.trim (x✝¹.trim % x✝.trim)

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

Raw monic Euclidean gcd.

Equations

• p.gcdMonic q = CompPoly.CPolynomial.Raw.gcdMonicWithFuel (Array.size p + Array.size q + 1) p q