Theorems · Theorem · category theory

HomologicalComplex.dgoEquivHomologicalComplex_counitIso

∀ {β : Type u_1} [inst : AddCommGroup β] (b : β) (V : Type u_2) [inst_1 : CategoryTheory.Category.{v_1, u_2} V]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms V],
  (HomologicalComplex.dgoEquivHomologicalComplex b V).counitIso =
    HomologicalComplex.dgoEquivHomologicalComplexCounitIso b V

Defined in

Mathlib.Algebra.Homology.DifferentialObject

Cited by

0 results in Mathlib

Foundations

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

Assumes

AddCommGroupCategoryTheory.CategoryCategoryTheory.Limits.HasZeroMorphisms