English
The coefficient of d of X^n · p equals coeff (d-n) p if n ≤ d, otherwise 0.
Русский
Коэффициент при d у X^n · p равен coeff (d-n) p, если n ≤ d, иначе 0.
LaTeX
$$$\\forall R\\ [\\operatorname{Semiring} R] (p : \\!R\\llbracket X\\rrbracket) (n d : \\mathbb{N}),\\ \\operatorname{coeff}(d)(X^n \\cdot p) = \\operatorname{ite}(n \\le d)(\\operatorname{coeff}(d-n) p)\\ 0$$$
Lean4
theorem coeff_X_pow_mul' (p : R⟦X⟧) (n d : ℕ) : coeff d (X ^ n * p) = ite (n ≤ d) (coeff (d - n) p) 0 :=
by
split_ifs with h
· rw [← tsub_add_cancel_of_le h, coeff_X_pow_mul]
simp
· refine (coeff_mul _ _ _).trans (Finset.sum_eq_zero fun x hx => ?_)
rw [coeff_X_pow, if_neg, zero_mul]
have := mem_antidiagonal.mp hx
rw [add_comm] at this
exact ((le_of_add_le_right this.le).trans_lt <| not_le.mp h).ne
