coeff_mul_X_sub_C — Mathlib

English

For p ∈ R[X], r ∈ R and a ∈ ℕ, coeff(p · (X − C r)) (a+1) = coeff p a − coeff p (a+1) · r.

Русский

Для p ∈ R[X], r ∈ R и a ∈ ℕ: coeff(p · (X − C r)) (a+1) = coeff p a − coeff p (a+1) · r.

LaTeX

$$$ p \in R[X], r \in R, a \in \mathbb{N} \Rightarrow \operatorname{coeff}(p \cdot (X - C r))(a+1) = \operatorname{coeff}(p)(a) - \operatorname{coeff}(p)(a+1) \cdot r $$$

Lean4

theorem coeff_mul_X_sub_C {p : R[X]} {r : R} {a : ℕ} :
    coeff (p * (X - C r)) (a + 1) = coeff p a - coeff p (a + 1) * r := by simp [mul_sub]

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