Univariate Division Correctness

Correctness theorems for division-style univariate polynomial algorithms.

theorem CompPoly.CPolynomial.divByMonic_toPoly_eq_divByMonic {R : Type u_1} [CommRing R] [BEq R] [LawfulBEq R] [Nontrivial R] (p q : CPolynomial R) (hmonic : q.monic = true) : (p.divByMonic q).toPoly = p.toPoly /ₘ q.toPoly

CompPoly's divByMonic is correct w.r.t. Mathlib's divByMonic

theorem CompPoly.CPolynomial.modByMonic_toPoly_eq_modByMonic {R : Type u_1} [CommRing R] [BEq R] [LawfulBEq R] [Nontrivial R] (p q : CPolynomial R) (hmonic : q.monic = true) : (p.modByMonic q).toPoly = p.toPoly %ₘ q.toPoly

CompPoly's modByMonic is correct w.r.t. Mathlib's modByMonic

theorem CompPoly.CPolynomial.modByMonic_add_mul_divByMonic {R : Type u_1} [CommRing R] [BEq R] [LawfulBEq R] [Nontrivial R] (p q : CPolynomial R) (hmonic : q.monic = true) : p.modByMonic q + q * p.divByMonic q = p

Euclidean division identity for a monic divisor, stated directly on CPolynomial: p.modByMonic q + q * p.divByMonic q = p whenever q is monic.

This holds over an arbitrary commutative ring, so it instantiates at nested coefficient rings, e.g. CBivariate R = CPolynomial (CPolynomial R), giving Euclidean division by any monic divisor in the outer variable.

theorem CompPoly.CPolynomial.leadingCoeff_inv_smul_monic {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (p : CPolynomial R) (hp : p ≠ 0) : (p.leadingCoeff⁻¹ • p).monic = true

Any nonzero polynomial scaled by the inverse of its leading coefficient is monic.

theorem CompPoly.CPolynomial.div_toPoly_eq_divByMonic {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (p q : CPolynomial R) (hq : q ≠ 0) : (p.div q).toPoly = q.leadingCoeff⁻¹ • p.toPoly /ₘ q.leadingCoeff⁻¹ • q.toPoly

Equality between CompPoly's div and Mathlib's divByMonic

theorem CompPoly.CPolynomial.mod_toPoly_eq_modByMonic {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (p q : CPolynomial R) (hq : q ≠ 0) : (p.mod q).toPoly = q.leadingCoeff⁻¹ • p.toPoly %ₘ q.leadingCoeff⁻¹ • q.toPoly

Equality between CompPoly's mod and Mathlib's modByMonic

theorem CompPoly.CPolynomial.div_toPoly_eq_div {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (p q : CPolynomial R) : (p.div q).toPoly = p.toPoly / q.toPoly

CompPoly's div is correct w.r.t. Mathlib's div.

theorem CompPoly.CPolynomial.mod_toPoly_eq_smul_mod {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (p q : CPolynomial R) : (p.mod q).toPoly = q.leadingCoeff⁻¹ • (p.toPoly % q.toPoly)

CompPoly's mod is Mathlib's % scaled by q.leadingCoeff⁻¹.

theorem CompPoly.CPolynomial.exactDiv_toPoly_iff {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (G V f : CPolynomial R) (hV : V.toPoly ≠ 0) : G.toPoly = f.toPoly * V.toPoly ↔ G.mod V = 0 ∧ (G / V).toPoly = f.toPoly

Exact-division bridge: G.toPoly factors as f.toPoly * V.toPoly iff the computable mod vanishes and the computable division recovers f.

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

The reversal monic remainder agrees with the canonical monic remainder.