ofScalarsSum — Mathlib

English

The sum of the scalar series corresponds to the sum over n of scalar multiples: ofScalarsSum c x = ∑_{n≥0} c(n) x^n.

Русский

Сумма скалярной серии соответствует сумме по всем n: ofScalarsSum c x = ∑_{n≥0} c(n) x^n.

LaTeX

$$$\operatorname{ofScalarsSum} c (x) = \sum_{n=0}^{\infty} c(n) \; x^{n}$$$

Lean4

/-- The sum of the formal power series. Takes the value `0` outside the radius of convergence. -/
noncomputable def ofScalarsSum :=
  (ofScalars E c).sum

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