coeff_mul_X — Mathlib

English

For p ∈ R[X] and n ∈ ℕ, the coefficient of (p · X) at n+1 equals the coefficient of p at n.

Русский

Для p ∈ R[X] и n ∈ ℕ, коэффициент (p · X) при степени n+1 равен коэффициенту p при степени n.

LaTeX

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

Lean4

@[simp]
theorem coeff_mul_X (p : R[X]) (n : ℕ) : coeff (p * X) (n + 1) = coeff p n := by
  simpa only [pow_one] using coeff_mul_X_pow p 1 n

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