hsum_ofFinsupp — Mathlib

English

The hsum of a finsupp-encoded Hahn series equals the sum of its coefficients.

Русский

Сумма по финсупп–кодированному гамма-рядy равна сумме его коэффициентов.

LaTeX

$$$ (ofFinsupp f).hsum = f.sum (\lambda _ => id) $$$

Lean4

@[simp]
theorem hsum_ofFinsupp {f : α →₀ HahnSeries Γ R} : (ofFinsupp f).hsum = f.sum fun _ => id :=
  by
  ext g
  simp only [coeff_hsum, coe_ofFinsupp, Finsupp.sum]
  simp_rw [← coeff.addMonoidHom_apply, id]
  rw [map_sum, finsum_eq_sum_of_support_subset]
  intro x h
  simp only [mem_coe, Finsupp.mem_support_iff, Ne]
  contrapose! h
  simp [h]

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