Theorems · Theorem · category theory

ChainComplex.of.congr_simp

∀ {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 d_1 : (n : α) → X (n + 1) ⟶ X n) (e_d : d = d_1)
  (sq : ∀ (n : α), CategoryTheory.CategoryStruct.comp (d (n + 1)) (d n) = 0),
  ChainComplex.of X d sq = ChainComplex.of X d_1 ⋯

Defined in

Mathlib.CategoryTheory.Abelian.Projective.Resolution

Cited by

0 results in Mathlib

Foundations

Depth 12 from the axioms · uses propext, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasZeroMorphismsAddRightCancelSemigroupOneDecidableEq