theorem Hex.DensePoly.pseudoDivMod_unique {S : Type u} [Lean.Grind.CommRing S] [DecidableEq S] [Div S] [ExactDivLaws S] (f g q r : DensePoly S) (hg : g ≠ 0) (hgf : g.size ≤ f.size) (hrec : scale (g.leadingCoeff ^ (f.size - g.size + 1)) f = q * g + r) (hr : r.size < g.size) : f.pseudoDivMod g = (q, r)

Reconstruction and the strict remainder bound uniquely characterize pseudoDivMod on an ordered nonzero input pair.

theorem Hex.DensePoly.pseudoDivMod_scale_left {S : Type u} [Lean.Grind.CommRing S] [DecidableEq S] [Div S] [ExactDivLaws S] (f g : DensePoly S) {a : S} (ha : a ≠ 0) (hg : g ≠ 0) (hgf : g.size ≤ f.size) : (scale a f).pseudoDivMod g = (scale a (f.pseudoDivMod g).fst, scale a (f.pseudoDivMod g).snd)

Scaling the dividend scales both pseudo-division outputs.

theorem Hex.DensePoly.pseudoDivMod_scale_right {S : Type u} [Lean.Grind.CommRing S] [DecidableEq S] [Div S] [ExactDivLaws S] (f g : DensePoly S) {a : S} (ha : a ≠ 0) (hg : g ≠ 0) (hgf : g.size ≤ f.size) : have d := f.size - g.size + 1; f.pseudoDivMod (scale a g) = (scale (a ^ (d - 1)) (f.pseudoDivMod g).fst, scale (a ^ d) (f.pseudoDivMod g).snd)

Scaling the divisor by a scales the pseudo-quotient by a^(d-1) and the pseudo-remainder by a^d, where d is the number of cancellation rounds.