Theorems · Theorem · category theory

CategoryTheory.TwistShiftData.assoc

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type w} [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] (self : CategoryTheory.TwistShiftData C A) (a b c : A),
  self.z (a + b) c * self.z a b = self.z a (b + c) * self.z b c

Defined in

Mathlib.CategoryTheory.Shift.Twist

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryAddMonoidCategoryTheory.HasShift