univ_sum_single — Mathlib

English

Over a finite type, the universal sum of single elements reconstructs the finsupp.

Русский

Для конечного типа единичные суммы по всем элементам восстанавливают финспп.

LaTeX

$$$$ \sum_{a \in \mathrm{univ}} \mathrm{single}_a (f(a)) = f $$$$

Lean4

/-- The `Finsupp` version of `Finset.univ_sum_single` -/
@[simp]
theorem univ_sum_single [Fintype α] [AddCommMonoid M] (f : α →₀ M) : ∑ a : α, single a (f a) = f := by
  classical
  refine DFunLike.coe_injective ?_
  simp_rw [coe_finset_sum, single_eq_pi_single, Finset.univ_sum_single]

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