ofScalarsSum_eq_tsum — Mathlib

English

Equivalently, the scalar sum equals the tsum representation: for all x, ofScalarsSum c x = tsum_n c(n) x^n.

Русский

Эквивалентно: сумма скаляров равна представлению через tsum: для всех x верно, что ofScalarsSum c x = tsum_n c(n) x^n.

LaTeX

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

Lean4

theorem ofScalarsSum_eq_tsum : ofScalarsSum c = fun (x : E) => ∑' n : ℕ, c n • x ^ n :=
  funext (ofScalars_sum_eq c)

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