hasSum_of_monomials_self — Mathlib

English

A multivariate power series is the sum, in the sense of a summable family, of its monomials indexed by the multi-exponent d ∈ σ →₀ ℕ.

Русский

Для многофакторной степенной серии существует разложение по мономиалам: она есть сумма её мономиальных членов по индексу d ∈ σ →₀ ℕ (суммируемое семейство).

LaTeX

$$$\text{HasSum}\left(\lambda d:σ\to_{0}ℕ, \text{monomial}(d, \text{coeff}(d,f))\right)\ f$$$

Lean4

/-- A multivariate power series is the sum (in the sense of summable families) of its monomials -/
theorem hasSum_of_monomials_self (f : MvPowerSeries σ R) : HasSum (fun d : σ →₀ ℕ => monomial d (coeff d f)) f :=
  by
  rw [Pi.hasSum]
  intro d
  simpa using hasSum_single d (fun d' h ↦ coeff_monomial_ne h.symm _)

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