coeffList_C_mul — Mathlib

English

If x ≠ 0 and P is a polynomial, then the coefficient list of Cx · P is obtained by multiplying each coefficient of P by x.

Русский

Если x ≠ 0 и P — полином, то coeffList(Cx · P) получается путём умножения каждого коэффициента P на x.

LaTeX

$$$ (C x * P).coeffList = P.coeffList.map (x * \\cdot) $ при x ≠ 0$$

Lean4

theorem coeffList_C_mul {x : R} (hx : x ≠ 0) : (C x * P).coeffList = P.coeffList.map (x * ·) :=
  by
  by_cases hp : P = 0
  · simp [hp]
  · simp [coeffList, Polynomial.degree_C hx]

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