univ_sum_single_apply' — Mathlib

English

Another variant: summing single j m over all j and evaluating at i yields m.

Русский

Еще один вариант: сумма по j единичного элемента на m по всем j при i даёт m.

LaTeX

$$$$ \sum_{j \in \mathrm{univ}} \mathrm{single}_j (m) (i) = m $$$$

Lean4

@[simp]
theorem univ_sum_single_apply' [AddCommMonoid M] [Fintype α] (i : α) (m : M) : ∑ j : α, single j m i = m :=
  by
  simp_rw [single, coe_mk]
  classical rw [Finset.sum_pi_single]
  simp

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