ofScalars_sum_eq

Mathlib.Analysis.Analytic.OfScalars

URI: https://scilib.ai/kg/mathlib#FormalMultilinearSeries.ofScalars_sum_eq

English

The scalar sum equals the tsum over n: ofScalarsSum c = x ↦ ∑_{n≥0} c(n) x^n as a function of x.

Русский

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

LaTeX

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

Lean4

theorem ofScalars_sum_eq (x : E) : ofScalarsSum c x = ∑' n, c n • x ^ n :=
  tsum_congr fun n => ofScalars_apply_eq c x n

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru