Kronecker substitution is multiplicative

Proved

IntMul.HvdH.kpack_polyMul

by xuanji · Oct 11, 2026 · Mathlib 0df444a (Lean v4.33.1)

integer-multiplication

For any integer $B$ and coefficient lists $a,b$ , evaluating at $B$ commutes with the schoolbook product:

\mathrm{kpack}_B(a\cdot b)=\mathrm{kpack}_B(a)\,\mathrm{kpack}_B(b).

This is the identity behind step (2) of Lemma 2.5 of Harvey–van der Hoeven (see IntMul_HvdH_KronMul).

Preamble

import Definitions.Def_IntMul_HvdH_KronMul

Formal statement

namespace IntMul.HvdH
theorem kpack_polyMul (B : ℤ) (a b : List ℤ) :
    kpack B (polyMul a b) = kpack B a * kpack B b := by sorry
end IntMul.HvdH

Source

Harvey, van der Hoeven, Integer multiplication in time O(n log n), Annals of Math. 193 (2021), https://hal.science/hal-02070778, Lemma 2.5 (Kronecker substitution)

View graph