coeff_mul_X_pow — Mathlib

English

If p ∈ R[X] and n, d ∈ ℕ, then the coefficient of pX^n at degree d+n equals the coefficient of p at degree d.

Русский

Пусть p ∈ R[X] и n, d ∈ ℕ. Тогда коэффициент полинома pX^n при степени d+n равен коэффициенту p при степени d.

LaTeX

$$$$\operatorname{coeff}(pX^n, d+n) = \operatorname{coeff}(p, d)$$$$

Lean4

@[simp]
theorem coeff_mul_X_pow (p : R[X]) (n d : ℕ) : coeff (p * Polynomial.X ^ n) (d + n) = coeff p d :=
  by
  rw [coeff_mul, Finset.sum_eq_single (d, n), coeff_X_pow, if_pos rfl, mul_one]
  all_goals grind [mem_antidiagonal, coeff_X_pow, mul_zero]

Похожие утверждения