English
For p ∈ R[X] and n, d ∈ ℕ, the coefficient of (p · X^n) at d equals coeff(p, d - n) if n ≤ d, and 0 otherwise.
Русский
Для p ∈ R[X] и n, d ∈ ℕ, коэффициент (p · X^n) при степени d равен coeff(p, d − n), если n ≤ d, иначе 0.
LaTeX
$$$$\operatorname{coeff}(pX^n, d) = \begin{cases} \operatorname{coeff}(p, d-n), & n \le d, \\ 0, & n > d. \end{cases}$$$$
Lean4
theorem coeff_mul_X_pow' (p : R[X]) (n d : ℕ) : (p * X ^ n).coeff d = ite (n ≤ d) (p.coeff (d - n)) 0 :=
by
split_ifs with h
· rw [← tsub_add_cancel_of_le h, coeff_mul_X_pow, add_tsub_cancel_right]
· refine (coeff_mul _ _ _).trans (Finset.sum_eq_zero fun x hx => ?_)
rw [coeff_X_pow, if_neg, mul_zero]
exact ((le_of_add_le_right (mem_antidiagonal.mp hx).le).trans_lt <| not_le.mp h).ne
