Theorems · Theorem · category theory

ComplexShape.Associative.assoc

∀ {I₁ : Type u_1} {I₂ : Type u_2} {I₃ : Type u_3} {I₁₂ : Type u_4} {I₂₃ : Type u_5} {J : Type u_6}
  {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {c₃ : ComplexShape I₃} {c₁₂ : ComplexShape I₁₂} {c₂₃ : ComplexShape I₂₃}
  {c : ComplexShape J} {inst : TotalComplexShape c₁ c₂ c₁₂} {inst_1 : TotalComplexShape c₁₂ c₃ c}
  {inst_2 : TotalComplexShape c₂ c₃ c₂₃} {inst_3 : TotalComplexShape c₁ c₂₃ c} [self : c₁.Associative c₂ c₃ c₁₂ c₂₃ c]
  (i₁ : I₁) (i₂ : I₂) (i₃ : I₃), c₁₂.π c₃ c (c₁.π c₂ c₁₂ (i₁, i₂), i₃) = c₁.π c₂₃ c (i₁, c₂.π c₃ c₂₃ (i₂, i₃))

Defined in

Mathlib.Algebra.Homology.ComplexShapeSigns

Cited by

1 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms

Assumes

ComplexShape.Associative