theorem
Hex.DensePoly.PseudoDivMod.reconstruct
{R : Type u}
[CommRing R]
[DecidableEq R]
(f g : DensePoly R)
(hg : g ≠ 0)
(hgf : g.size ≤ f.size)
:
have q := (f.pseudoDivMod g).1;
have r := (f.pseudoDivMod g).2;
Polynomial.C (g.leadingCoeff ^ (f.size - g.size + 1)) * HexPolyMathlib.toPolynomial f = HexPolyMathlib.toPolynomial q * HexPolyMathlib.toPolynomial g + HexPolyMathlib.toPolynomial r
The executable reconstruction identity transported to Mathlib polynomials.
theorem
Hex.DensePoly.PseudoDivMod.quotient_degree
{R : Type u}
[CommRing R]
[DecidableEq R]
(f g : DensePoly R)
(hg : g ≠ 0)
(hgf : g.size ≤ f.size)
:
A pseudo-quotient fits in the formal-degree gap required by Mathlib's resultant row-operation theorem.
theorem
Hex.DensePoly.PseudoDivMod.remainder_degree
{R : Type u}
[CommRing R]
[DecidableEq R]
(f g : DensePoly R)
(hg : g ≠ 0)
:
HexPolyMathlib.toPolynomial (f.pseudoDivMod g).2 = 0 ∨ (HexPolyMathlib.toPolynomial (f.pseudoDivMod g).2).natDegree < (HexPolyMathlib.toPolynomial g).natDegree
A pseudo-remainder is zero or has strictly smaller Mathlib degree than
the nonzero divisor. The disjunction records Mathlib's default degree 0 for
the zero polynomial, including the constant-divisor case.
theorem
Hex.DensePoly.PseudoDivMod.resultant_step
{R : Type u}
[CommRing R]
[DecidableEq R]
(f g : DensePoly R)
(hg : g ≠ 0)
(hgf : g.size ≤ f.size)
:
have r := (f.pseudoDivMod g).2;
have F := HexPolyMathlib.toPolynomial f;
have G := HexPolyMathlib.toPolynomial g;
have P := HexPolyMathlib.toPolynomial r;
have n := F.natDegree;
have m := G.natDegree;
(g.leadingCoeff ^ (f.size - g.size + 1)) ^ m * F.resultant G n m = (-1) ^ (n * m) * G.resultant P m n
One fraction-free pseudo-division step transports the formal-degree
resultant from (f,g) to (g,r), including the Sylvester swap sign.
theorem
Hex.DensePoly.PseudoDivMod.resultant_step_degree
{R : Type u}
[CommRing R]
[DecidableEq R]
(f g : DensePoly R)
(hg : g ≠ 0)
(hgf : g.size ≤ f.size)
:
have r := (f.pseudoDivMod g).2;
have F := HexPolyMathlib.toPolynomial f;
have G := HexPolyMathlib.toPolynomial g;
have P := HexPolyMathlib.toPolynomial r;
have n := F.natDegree;
have m := G.natDegree;
have k := P.natDegree;
(g.leadingCoeff ^ (f.size - g.size + 1)) ^ m * F.resultant G n m = (-1) ^ (n * m) * (g.leadingCoeff ^ (n - k) * G.resultant P m k)
The pseudo-division resultant identity with the remainder returned to its actual default degree. The compensating leading-coefficient power records the formal-degree promotion explicitly.