English
Multiplication by X^n shifts coefficients: the coefficient of degree d+n in p·X^n equals the coefficient of degree d in p.
Русский
Умножение на X^n сдвигает коэффициенты: коэффициент при степени d+n в p·X^n равен коэффициенту при степени d в p.
LaTeX
$$$\\forall R\\ [\\operatorname{Semiring} R], \\forall p \\in R\\llbracket X\\rrbracket, \\forall n,d \\in \\mathbb{N},\\ \\operatorname{coeff}(d+n)(p\\cdot X^n) = \\operatorname{coeff}(d)p$$$
Lean4
@[simp]
theorem coeff_mul_X_pow (p : R⟦X⟧) (n d : ℕ) : coeff (d + n) (p * X ^ n) = coeff d p :=
by
rw [coeff_mul, Finset.sum_eq_single (d, n), coeff_X_pow, if_pos rfl, mul_one]
· rintro ⟨i, j⟩ h1 h2
rw [coeff_X_pow, if_neg, mul_zero]
rintro rfl
apply h2
rw [mem_antidiagonal, add_right_cancel_iff] at h1
subst h1
rfl
· exact fun h1 => (h1 (mem_antidiagonal.2 rfl)).elim
