English
Summing a function that is zero except at a fixed index a yields the corresponding value if a is in the support, otherwise 0.
Русский
Сумма функции, равной нулю кроме фиксированного индекса a, даёт значение при a, если a входит в поддерживаемое множество, иначе 0.
LaTeX
$$$$ (f.sum (\\\\lambda x \\\\linebreak v, \\\\; if x = a \\\\ then b x v \\\\ else 0)) = if a \\\\in f.support \\\\ then b a (f.coeff a) \\\\ else 0 $$$$
Lean4
/-- Analogue of `Finsupp.sum_ite_eq'` for `SkewMonoidAlgebra`. -/
@[simp]
theorem sum_ite_eq' {N : Type*} [AddCommMonoid N] [DecidableEq G] (f : SkewMonoidAlgebra k G) (a : G) (b : G → k → N) :
(f.sum fun (x : G) (v : k) ↦ if x = a then b x v else 0) = if a ∈ f.support then b a (f.coeff a) else 0 := by
simp only [sum_def', f.toFinsupp.support.sum_ite_eq', support]
