coeff_X_pow_mul — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem coeff_X_pow_mul (p : R[X]) (n d : ℕ) : coeff (Polynomial.X ^ n * p) (d + n) = coeff p d := by
  rw [(commute_X_pow p n).eq, coeff_mul_X_pow]

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