single_sum

Mathlib.Algebra.BigOperators.Finsupp.Basic

URI: https://scilib.ai/kg/mathlib#Finsupp.single_sum

← MathLib Explorer

English

If g maps a second argument 0 to 1, then (-g).prod h = g.prod (λ a b, h a (-b)).

Русский

Если g(i,0)=1 для всех i, то (-g).prod h = g.prod (λ a b, h a (-b)).

LaTeX

$$$$ (-g).prod h = g.prod (\\\\lambda a b, h a (-b)) $$$$

Lean4

theorem single_sum [Zero M] [AddCommMonoid N] (s : ι →₀ M) (f : ι → M → N) (a : α) :
    single a (s.sum f) = s.sum fun d c => single a (f d c) :=
  single_finset_sum _ _ _

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru