def Hex.DensePoly.diagonalMulCoeffTerm {S : Type u_1} [Zero S] [DecidableEq S] [Mul S] (p q : DensePoly S) (n i : Nat) : S

The i-th summand of the degree-n convolution diagonal of p * q, p.coeff i * q.coeff (n - i), zeroed once the degree guard n < i fires; the single-index term that mulCoeffSum is reorganised into.

Equations

• p.diagonalMulCoeffTerm q n i = if n < i then 0 else p.coeff i * q.coeff (n - i)

theorem Hex.DensePoly.mulCoeffSum_eq_diagonal {S : Type u_1} [Lean.Grind.CommRing S] [DecidableEq S] (p q : DensePoly S) (n : Nat) : p.mulCoeffSum q n = List.foldl (fun (acc : S) (i : Nat) => acc + p.diagonalMulCoeffTerm q n i) 0 (List.range p.size)

The schoolbook coefficient mulCoeffSum p q n equals the diagonal sum Σ_{i < p.size} diagonalMulCoeffTerm p q n i; the correspondence from the executable loop order to the convolution form used in the ring-law proofs.

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

Pull a zero-based negation out of a product and commute the factors: p * (0 - q) = 0 - q * p. A Mathlib-free DensePoly ring shim (the type carries only Lean.Grind.CommRing, so neg_mul/mul_comm are unavailable).

theorem Hex.DensePoly.scale_mul {S : Type u_1} [Lean.Grind.CommRing S] [DecidableEq S] (a : S) (p q : DensePoly S) : scale a (p * q) = scale a p * q

Pull a coefficient scalar through the left polynomial factor.

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

Commutativity of DensePoly multiplication. Hand-proved because DensePoly carries only Lean.Grind.CommRing, not Mathlib's CommRing, so mul_comm is unavailable.

theorem Hex.DensePoly.mul_scale {S : Type u_1} [Lean.Grind.CommRing S] [DecidableEq S] (a : S) (p q : DensePoly S) : scale a (p * q) = p * scale a q

Pull a coefficient scalar through the right polynomial factor.

theorem Hex.DensePoly.add_sub_add_swap {S : Type u_1} [Lean.Grind.CommRing S] [DecidableEq S] (x y z : DensePoly S) : x + y - (z + x) = y + (0 - z)

Cancellation rearrangement (x + y) - (z + x) = y + (0 - z), used to simplify mixed add/sub combinations arising in the Euclidean update steps.

theorem Hex.DensePoly.add_sub_add_left {S : Type u_1} [Lean.Grind.CommRing S] [DecidableEq S] (x y z : DensePoly S) : x + y - (x + z) = y + (0 - z)

Cancellation rearrangement (x + y) - (x + z) = y + (0 - z).

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

Commutativity of DensePoly addition (the Mathlib-free add_comm).

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

Associativity of DensePoly addition (the Mathlib-free add_assoc).

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

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

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

Rewrite a DensePoly subtraction as addition of the zero-based negation: p - q = p + (0 - q).

theorem Hex.DensePoly.rat_mulCoeffSum_derivative_product_rule (p q : DensePoly Rat) (n : Nat) : ↑(n + 1) * p.mulCoeffSum q (n + 1) = p.derivative.mulCoeffSum q n + p.mulCoeffSum q.derivative n

Rational-coefficient specialization of mulCoeffSum_derivative_product_rule: the (n+1) scaling factor is cast into Rat.

theorem Hex.DensePoly.mulCoeffSum_derivative_product_rule {S : Type u_1} [Lean.Grind.CommRing S] [DecidableEq S] (p q : DensePoly S) (n : Nat) : ↑(n + 1) * p.mulCoeffSum q (n + 1) = p.derivative.mulCoeffSum q n + p.mulCoeffSum q.derivative n

Coefficient-level product rule: (n+1) times the order-(n+1) product coefficient sum equals the sum of the two derivative product coefficient sums. This is the per-coefficient identity underlying derivative_mul.

theorem Hex.DensePoly.derivative_mul {S : Type u_1} [Lean.Grind.CommRing S] [DecidableEq S] (p q : DensePoly S) : (p * q).derivative = p.derivative * q + p * q.derivative

Leibniz product rule for the formal DensePoly derivative: derivative (p * q) = derivative p * q + p * derivative q.

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

Associativity of DensePoly multiplication (the Mathlib-free mul_assoc).

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

Left distributivity for DensePoly: p * (q + r) = p * q + p * r.

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

Right distributivity for DensePoly: (p + q) * r = p * r + q * r.

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

Right identity for polynomial multiplication over a commutative ring: p * 1 = p. A grind normalization lemma; the Bézout and division routines cancel multiplications by the unit polynomial through it.

instance Hex.DensePoly.instAssociativeMulDensePoly {S : Type u_1} [Lean.Grind.CommRing S] [DecidableEq S] : Std.Associative fun (x1 x2 : DensePoly S) => x1 * x2

DensePoly S is a multiplicative monoid: these Std instances let the shared List.foldl_mul_* algebra (and the standard List.foldl_assoc) apply to fold-products of polynomials such as FpPoly/ZPoly.

instance Hex.DensePoly.instLawfulIdentityMulDensePoly {S : Type u_1} [Lean.Grind.CommRing S] [DecidableEq S] : Std.LawfulIdentity (fun (x1 x2 : DensePoly S) => x1 * x2) 1

theorem Hex.DensePoly.monomial_mul_monomial {S : Type u_1} [Lean.Grind.CommRing S] [DecidableEq S] (m k : Nat) (c d : S) : monomial m c * monomial k d = monomial (m + k) (c * d)

Product of two monomials: xⁱ * cⱼ * xʲ = cᵢcⱼ * xⁱ⁺ʲ.