English
Coefficient of X^n times a power series p: the degree d coefficient equals coeff_{d-n} p when d ≥ n, otherwise 0.
Русский
Коэффициент при степени d у X^n·p равен coeff_{d-n} p, если d ≥ n, иначе 0.
LaTeX
$$$\\forall R\\ [\\operatorname{Semiring} R], \\forall p \\in R\\llbracket X\\rrbracket, \\forall n,d \\in \\mathbb{N},\\ \\operatorname{coeff}(d)(X^n \\cdot p) = \\begin{cases} \\operatorname{coeff}(d-n)p, & n \\le d \\\\ 0, & \\text{иначе} \\end{cases}$$$
Lean4
@[simp]
theorem coeff_X_pow_mul (p : R⟦X⟧) (n d : ℕ) : coeff (d + n) (X ^ n * p) = coeff d p :=
by
rw [coeff_mul, Finset.sum_eq_single (n, d), coeff_X_pow, if_pos rfl, one_mul]
· rintro ⟨i, j⟩ h1 h2
rw [coeff_X_pow, if_neg, zero_mul]
rintro rfl
apply h2
rw [mem_antidiagonal, add_comm, add_right_cancel_iff] at h1
subst h1
rfl
· rw [add_comm]
exact fun h1 => (h1 (mem_antidiagonal.2 rfl)).elim
