Raw Univariate Polynomial Division

Division algorithms for raw computable univariate polynomials.

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.

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] [Field 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 x✝¹ x✝ = (0, x✝¹)

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.

Equations

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

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.

Equations

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

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 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 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 }