Theorems · Theorem · category theory

CategoryTheory.ShiftMkCore.shiftFunctorAdd_eq

∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddMonoid A]
  (h : CategoryTheory.ShiftMkCore C A) (a b : A), CategoryTheory.shiftFunctorAdd C a b = h.add a b

Defined in

Mathlib.CategoryTheory.Shift.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryAddMonoid