Coefficients of shifted polynomials with a degree bound

Multiplication by X ^ l shifts a polynomial's coefficients by l. When its degree is bounded by n, the shifted coefficients vanish outside the window from l to l + n. This identity identifies bounded coefficient rows with coefficients of shifted polynomials.

theorem Polynomial.coeff_X_pow_mul_of_natDegree_le {R : Type u_1} [Semiring R] {p : Polynomial R} {n : ℕ} (hp : p.natDegree ≤ n) (l d : ℕ) : (X ^ l * p).coeff d = if l ≤ d ∧ d ≤ l + n then p.coeff (d - l) else 0

The coefficients of X ^ l * p vanish outside the window from l to l + n when p.natDegree ≤ n.