mapCoeffs_apply — Mathlib

English

For any polynomial p and index i, the i-th coefficient of mapCoeffs(d)(p) equals d applied to the i-th coefficient of p.

Русский

Для любого полиномa p и индекса i, i-й коэффициент mapCoeffs(d)(p) равен применению d к i-му коэффициенту p.

LaTeX

$$$\text{coeff}_i(\mathrm{mapCoeffs}(p)) = d(\text{coeff}_i(p)).$$$

Lean4

@[simp]
theorem mapCoeffs_apply (p : A[X]) (i) : d.mapCoeffs p i = d (coeff p i) :=
  rfl

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