update_eq_add_sub_coeff — Mathlib

English

For any p ∈ R[X], n ∈ ℕ, a ∈ R, the updated polynomial p.update n a equals p plus C(a − coeff(p,n)) times X^n.

Русский

Для любого полинома p ∈ R[X], индекса n и элемента a ∈ R при обновлении коэффициент при X^n становится a; это достигается так: p.update n a = p + C(a − coeff(p,n)) · X^n.

LaTeX

$$$ p.update(n,a) = p + \mathrm{C}(a - p.coeff(n)) \cdot X^{n}$$$

Lean4

theorem update_eq_add_sub_coeff {R : Type*} [Ring R] (p : R[X]) (n : ℕ) (a : R) :
    p.update n a = p + Polynomial.C (a - p.coeff n) * Polynomial.X ^ n :=
  by
  ext
  rw [coeff_update_apply, coeff_add, coeff_C_mul_X_pow]
  split_ifs with h <;> simp [h]

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