sum_single_ite — Mathlib

English

For a finite type n, the sum over x ∈ n of Finsupp.single x (if i = x then a else 0) equals Finsupp.single i a.

Русский

Для конечного типа n сумма по x ∈ n Finsupp.single x (если i = x то a, иначе 0) равна Finsupp.single i a.

LaTeX

$$$\\sum_{x \\in n} \\mathrm{single}_x(\\mathbf{1}_{i=x}a) = \\mathrm{single}_i(a)$$$

Lean4

theorem _root_.Finset.sum_single_ite [Fintype n] (a : R) (i : n) :
    (∑ x : n, Finsupp.single x (if i = x then a else 0)) = Finsupp.single i a := by
  simp only [apply_ite (Finsupp.single _), Finsupp.single_zero, Finset.sum_ite_eq, if_pos (Finset.mem_univ _)]

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