coeff_hsum_eq_sum — Mathlib

English

The coefficient of the hsum at g equals the sum of the coefficients (over i) of each summand at g, taken over the support of s.coeff g.

Русский

Коэффициент суммы по Хану при g равен сумме коэффициентов по i от каждого слагаемого в сумме, взятой по опоре s.coeff g.

LaTeX

$$$s.hsum.coeff g = \\sum_{i \\in (s.coeff g).\\mathrm{support}} (s i).coeff g$$$

Lean4

theorem coeff_hsum_eq_sum {s : SummableFamily Γ R α} {g : Γ} :
    s.hsum.coeff g = ∑ i ∈ (s.coeff g).support, (s i).coeff g := by
  simp only [coeff_hsum, finsum_eq_sum _ (s.finite_co_support _), coeff_support]

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