as_tsum — Mathlib

English

If the coefficient space is a T2 (Hausdorff) space, then a multivariate power series f is equal to the tsum of its monomials, i.e., f equals the sum of its monomial contributions.

Русский

Если пространство коэффициентов T2, то многомерная степенная серия равна сумме по мономиалам.

LaTeX

$$$f = \operatorname{tsum}_{d:σ→₀ℕ} \text{monomial}(d, \text{coeff}(d,f))$$$

Lean4

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

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