English
The coefficient of d+(n) in p·X^n equals coeff d p if n ≤ d, otherwise 0.
Русский
Коэффициент при d+n в p·X^n равен coeff d p, если n ≤ d, иначе 0.
LaTeX
$$$\\forall R\\ [\\operatorname{Semiring} R] (p : R\\llbracket X\\rrbracket) (n d : \\mathbb{N}),\\ \\operatorname{coeff}(d)(p\\cdot X^n) = \\operatorname{ite}(n \\le d)(\\operatorname{coeff}(d-n)p)\\ 0$$$
Lean4
theorem coeff_mul_X_pow' (p : R⟦X⟧) (n d : ℕ) : coeff d (p * X ^ n) = ite (n ≤ d) (coeff (d - n) p) 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
