theorem Hex.DensePoly.monomial_one_mul_poly_eq_shift {S : Type u_1} [Lean.Grind.CommRing S] [DecidableEq S] (shift : Nat) (q : DensePoly S) : monomial shift 1 * q = DensePoly.shift shift q

Multiplication by a unit-coefficient monomial shifts coefficients upward.

theorem Hex.DensePoly.neg_mul_right_poly {S : Type u_1} [Lean.Grind.CommRing S] [DecidableEq S] (p q : DensePoly S) : (0 - p) * q = 0 - p * q

Negation passes through the left multiplicand: (0 - p) * q = 0 - p * q. A grind normalization lemma that lets sign manipulations in the extended-gcd recursion move the negation out to the product.

theorem Hex.DensePoly.add_mul_sub_cancel_right {S : Type u_1} [Lean.Grind.CommRing S] [DecidableEq S] (p t q r : DensePoly S) : (p + t) * q + (r - t * q) = p * q + r

Telescoping identity for an extended-Euclid update step: (p + t) * q + (r - t * q) = p * q + r.

theorem Hex.DensePoly.divMod_reconstruction_step {S : Type u_1} [Lean.Grind.CommRing S] [DecidableEq S] (quot term q rem : DensePoly S) : (quot + term) * q + (rem - term * q) = quot * q + rem

One long-division reconstruction step preserves the accumulated identity quot * q + rem.

theorem Hex.DensePoly.zero_mul {S : Type u_1} [Lean.Grind.CommRing S] [DecidableEq S] (p : DensePoly S) : 0 * p = 0

Left absorption for polynomial multiplication: 0 * p = 0. A grind normalization lemma so that products with a vanished factor collapse during the division and gcd proofs.

theorem Hex.DensePoly.zero_add {S : Type u_1} [Lean.Grind.CommRing S] [DecidableEq S] (p : DensePoly S) : 0 + p = p

Left identity for polynomial addition over a commutative ring: 0 + p = p. A grind normalization lemma so downstream proofs cancel leading zero summands.

theorem Hex.DensePoly.dvd_refl_poly {S : Type u_1} [Lean.Grind.CommRing S] [DecidableEq S] (p : DensePoly S) : p ∣ p

Reflexivity of DensePoly divisibility (the Mathlib-free dvd_refl).

theorem Hex.DensePoly.dvd_zero_poly {S : Type u_1} [Lean.Grind.CommRing S] [DecidableEq S] (p : DensePoly S) : p ∣ 0

Every DensePoly divides 0 (the Mathlib-free dvd_zero).

theorem Hex.DensePoly.dvd_mul_left_poly {S : Type u_1} [Lean.Grind.CommRing S] [DecidableEq S] {d p : DensePoly S} (q : DensePoly S) : d ∣ p → d ∣ q * p

Divisibility is preserved by multiplication on the left: d ∣ p → d ∣ q * p.

theorem Hex.DensePoly.dvd_add_poly {S : Type u_1} [Lean.Grind.CommRing S] [DecidableEq S] {d p q : DensePoly S} : d ∣ p → d ∣ q → d ∣ p + q

A common divisor of two DensePolys divides their sum.

theorem Hex.DensePoly.dvd_sub_poly {S : Type u_1} [Lean.Grind.CommRing S] [DecidableEq S] {d p q : DensePoly S} : d ∣ p → d ∣ q → d ∣ p - q

A common divisor of two DensePolys divides their (zero-based) difference.

theorem Hex.DensePoly.xgcd_bezout_of_divModLaws {S : Type u_1} [Lean.Grind.CommRing S] [DecidableEq S] [Div S] [DivModLaws S] (p q : DensePoly S) : have r := p.xgcd q; r.left * p + r.right * q = r.gcd

Bezout identity for xgcd, proved from DivModLaws for use when building the corresponding GcdLaws instance.

theorem Hex.DensePoly.gcd_dvd_left_of_divModLaws {S : Type u_1} [Lean.Grind.CommRing S] [DecidableEq S] [Div S] [DivModLaws S] (hsmall : ∀ (p q : DensePoly S), q.isZero = false → ¬0 < q.degree?.getD 0 → (p.divMod q).snd = 0) (p q : DensePoly S) : p.gcd q ∣ p

The gcd returned by xgcd divides the left input, assuming DivModLaws and the one-off hsmall fact for nonzero divisors of degree zero. This is intended for GcdLaws instance construction.

theorem Hex.DensePoly.gcd_dvd_right_of_divModLaws {S : Type u_1} [Lean.Grind.CommRing S] [DecidableEq S] [Div S] [DivModLaws S] (hsmall : ∀ (p q : DensePoly S), q.isZero = false → ¬0 < q.degree?.getD 0 → (p.divMod q).snd = 0) (p q : DensePoly S) : p.gcd q ∣ q

The gcd returned by xgcd divides the right input, assuming DivModLaws and the one-off hsmall fact for nonzero divisors of degree zero. This is intended for GcdLaws instance construction.

theorem Hex.DensePoly.dvd_gcd_of_divModLaws {S : Type u_1} [Lean.Grind.CommRing S] [DecidableEq S] [Div S] [DivModLaws S] (d p q : DensePoly S) : d ∣ p → d ∣ q → d ∣ p.gcd q

Any common divisor divides the gcd returned by xgcd; this packages the DivModLaws proof needed by GcdLaws instance construction.

theorem Hex.DensePoly.divModArray_reconstruction {S : Type u_1} [Lean.Grind.CommRing S] [DecidableEq S] (p q : DensePoly S) (scaleLead : S → S) (hcancel : ∀ (a : S), a - scaleLead a * q.leadingCoeff = Zero.zero) : (p.divModArray q scaleLead).fst * q + (p.divModArray q scaleLead).snd = p

Reconstruction identity for array-backed long division: under the cancellation hypothesis for scaleLead against the divisor's leading coefficient, the quotient/remainder pair returned by divModArray p q scaleLead satisfies q' * q + r' = p.

theorem Hex.DensePoly.divMod_reconstruction {S : Type u_1} [Lean.Grind.CommRing S] [DecidableEq S] [Div S] (p q : DensePoly S) (hcancel : ∀ (a : S), a - a / q.leadingCoeff * q.leadingCoeff = Zero.zero) : have qr := p.divMod q; qr.fst * q + qr.snd = p

Reconstruction identity for the executable long division wrapper.

theorem Hex.DensePoly.leadingCoeff_mul {S : Type u_1} [Lean.Grind.CommRing S] [DecidableEq S] (p q : DensePoly S) (hp : 0 < p.size) (hq : 0 < q.size) (hprod : p.leadingCoeff * q.leadingCoeff ≠ Zero.zero) : (p * q).leadingCoeff = p.leadingCoeff * q.leadingCoeff

Leading coefficient of a product, in the cancellation-free form needed over commutative rings. The explicit nonzero top-coefficient product hypothesis is the no-cancellation fact that callers over domains can derive from nonzero factors.

theorem Hex.DensePoly.divMod_eq_of_polynomial_mul {S : Type u_1} [Lean.Grind.CommRing S] [DecidableEq S] [Div S] (p q qq : DensePoly S) (hq_ne : q ≠ 0) (hexact : ∀ (a : S), a * q.leadingCoeff / q.leadingCoeff = a) (h_top_ne : ∀ (a : S), a ≠ Zero.zero → a * q.leadingCoeff ≠ Zero.zero) (hmul : qq * q = p) : p.divMod q = (qq, 0)

Public divMod identity for nonzero, non-monic exact-multiple inputs: if qq * q = p, the scaling function (· / q.leadingCoeff) exactly recovers any a from a * q.leadingCoeff, and the leading-coefficient product never cancels, then divMod p q = (qq, 0). The exactness and no-zero-divisor hypotheses replace the global cancellation invariant ∀ a, a - (a / q.leadingCoeff) * q.leadingCoeff = 0 required by divMod_reconstruction (which only holds in the monic case over Int).