Theorems · Theorem · category theory

Action.sum_hom

∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G]
  [inst_2 : CategoryTheory.Preadditive V] {X Y : Action V G} {ι : Type u_3} (f : ι → (X ⟶ Y)) (s : Finset ι),
  (s.sum f).hom = ∑ i ∈ s, (f i).hom

Defined in

Mathlib.CategoryTheory.Action.Limits

Cited by

0 results in Mathlib

Foundations

Depth 47 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryMonoidCategoryTheory.Preadditive