as_tsum — Mathlib

English

If the coefficient space is T2, then f equals the tsum of monomial terms: f = tsum_{d} monomial_d(coeff_d f).

Русский

Если пространство коэффициентов T2, то f равно tsum мономиальных членов: f = tsum_{d} monomial_d(coeff_d f).

LaTeX

$$$f = \mathrm{tsum}_{d \in \mathbb{N}} \mathrm{monomial}_d(\mathrm{coeff}_d f)$$$

Lean4

/-- If the coefficient space is T2, then the power series is `tsum` of its monomials -/
theorem as_tsum [T2Space R] (f : PowerSeries R) : f = tsum fun d : ℕ => monomial d (coeff d f) :=
  (HasSum.tsum_eq (hasSum_of_monomials_self f)).symm

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