smeval_eq_sum — Mathlib

English

For a Laurent polynomial f = ∑ n r_n T^n, the evaluation smeval at a unit x is the sum of the scalar actions of the coefficients: smeval(f, x) = ∑ n r_n · x^n.

Русский

Пусть f = ∑ n r_n T^n — лаурентовский полином. Значение smeval в единице x равно сумме: smeval(f, x) = ∑ n r_n · x^n.

LaTeX

$$$ \mathrm{smeval}(f, x) = \sum_{n \in \mathbb{Z}} r_n \, x^n $$$

Lean4

theorem smeval_eq_sum : f.smeval x = Finsupp.sum f fun n r => r • (x ^ n).val :=
  rfl

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