Theorems · Theorem · category theory

ChainComplex.of_d

∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  {α : Type u_2} [inst_2 : AddRightCancelSemigroup α] [inst_3 : One α] [inst_4 : DecidableEq α] (X : α → V)
  (d : (n : α) → X (n + 1) ⟶ X n) (j : α), ChainComplex.of.d X d (j + 1) j = d j

Defined in

Mathlib.Algebra.Homology.HomologicalComplex

Cited by

9 results in Mathlib

Foundations

Depth 7 from the axioms · uses no axioms

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasZeroMorphismsAddRightCancelSemigroupOneDecidableEq