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.xgcd_bezout_of_reconstruction {S : Type u_1} [Lean.Grind.CommRing S] [DecidableEq S] [Div S] (hspec : ∀ (p q : DensePoly S), q.isZero = false → have qr := p.divMod q; qr.fst * q + qr.snd = p) (p q : DensePoly S) : have r := p.xgcd q; r.left * p + r.right * q = r.gcd

Bezout correctness from the reconstruction law needed along the nonzero divisors actually visited by the Euclidean loop. This weaker interface lets generic fields use the executable gcd without constructing the unrelated remainder-congruence laws.

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.natDegree → (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.natDegree → (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.gcd_dvd_inputs_of_reconstruction {S : Type u_1} [Lean.Grind.CommRing S] [DecidableEq S] [Div S] (hspec : ∀ (p q : DensePoly S), q.isZero = false → have qr := p.divMod q; qr.fst * q + qr.snd = p) (hdegree : ∀ (p q : DensePoly S), q.isZero = false → 0 < q.natDegree → (p.divMod q).snd.natDegree < q.natDegree) (hsmall : ∀ (p q : DensePoly S), q.isZero = false → ¬0 < q.natDegree → (p.divMod q).snd = 0) (p q : DensePoly S) : p.gcd q ∣ p ∧ p.gcd q ∣ q

The executable gcd divides both inputs from only reconstruction, strict remainder descent, and the nonzero-constant remainder case.

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.coeff_mul_top {S : Type u_1} [Lean.Grind.CommRing S] [DecidableEq S] (p q : DensePoly S) (hp : 0 < p.size) (hq : 0 < q.size) : (p * q).coeff (p.size - 1 + (q.size - 1)) = p.coeff (p.size - 1) * q.coeff (q.size - 1)

The top coefficient of a product of nonzero dense polynomials over any commutative ring is the product of their top coefficients.

theorem Hex.DensePoly.size_mul_of_top_ne {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).size = p.size + q.size - 1

Stored size of a product when its top coefficient does not cancel.

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).