aeval_eq_sum — Mathlib

English

For ha and f, the evaluation map equals the sum of the series of coefficients times a^d; i.e., aeval ha f = tsum (d ↦ coeff d f • a^d).

Русский

Для ha и f отображение эвалюации равно сумме ряда коэффициентов, умноженных на a^d; то есть aeval ha f = tsum (d ↦ coeff d f • a^d).

LaTeX

$$$ \operatorname{aeval}(ha)\!\, f = \operatorname{tsum}(d \mapsto \mathrm{coeff}_d f \cdot a^d) $$$

Lean4

theorem aeval_eq_sum (ha : HasEval a) (f : PowerSeries R) : aeval ha f = tsum fun d ↦ coeff d f • a ^ d :=
  (hasSum_aeval ha f).tsum_eq.symm

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