map_sum

Mathlib.CategoryTheory.Preadditive.AdditiveFunctor

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.map_sum

← MathLib Explorer

English

A additive functor preserves finite sums over a finite index set.

Русский

Добавитивный функтор сохраняет конечные суммы по конечному индексу.

LaTeX

$$$F.map(\\sum_{a\\in s} f(a)) = \\sum_{a\\in s} F.map(f(a))$$$

Lean4

@[simp]
nonrec theorem map_sum {X Y : C} {α : Type*} (f : α → (X ⟶ Y)) (s : Finset α) :
    F.map (∑ a ∈ s, f a) = ∑ a ∈ s, F.map (f a) :=
  map_sum F.mapAddHom f s

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

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

Разделы

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

Аффилиация

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