Documentation Verification Report

CM5b

📁 Source: Mathlib/Algebra/Homology/Factorizations/CM5b.lean

Statistics

Metric	Count
Definitions `I`, `homotopyEquiv`, `i`, `p`	4
Theorems `cm5b`, `I_X`, `I_d`, `degreewiseEpiWithInjectiveKernel_p`, `fac`, `fac_assoc`, `i_f_comp`, `i_f_comp_assoc`, `instInjectiveXIntI`, `instInjectiveXIntMappingConeIdI`, `instIsStrictlyGEBiprodIntMappingConeIdIOfHAddOfNat`, `instIsStrictlyGEI`, `instMonoFIntI`, `instMonoIntI`, `instQuasiIsoIntP`	15
Total	19

CochainComplex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cm5b` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CochainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.instCategory` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian` `instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `CategoryTheory.Abelian.hasBinaryBiproducts` `HomologicalComplex.instHasBinaryBiproduct` `cm5b.instIsStrictlyGEBiprodIntMappingConeIdIOfHAddOfNat` `cm5b.instMonoIntI` `cm5b.degreewiseEpiWithInjectiveKernel_p` `cm5b.instQuasiIsoIntP` `cm5b.fac`

CochainComplex.cm5b

Definitions

Name	Category	Theorems
`I` 📖	CompOp	14 math math: `fac`, `instIsStrictlyGEBiprodIntMappingConeIdIOfHAddOfNat`, `fac_assoc`, `instQuasiIsoIntP`, `instIsStrictlyGEI`, `instMonoFIntI`, `instInjectiveXIntI`, `instMonoIntI`, `i_f_comp`, `i_f_comp_assoc`, `I_d`, `degreewiseEpiWithInjectiveKernel_p`, `instInjectiveXIntMappingConeIdI`, `I_X`
`homotopyEquiv` 📖	CompOp	—
`i` 📖	CompOp	6 math math: `fac`, `fac_assoc`, `instMonoFIntI`, `instMonoIntI`, `i_f_comp`, `i_f_comp_assoc`
`p` 📖	CompOp	4 math math: `fac`, `fac_assoc`, `instQuasiIsoIntP`, `degreewiseEpiWithInjectiveKernel_p`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`I_X` 📖	mathematical	—	`HomologicalComplex.X` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `I` `CategoryTheory.Injective.under`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`
`I_d` 📖	mathematical	—	`HomologicalComplex.d` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `I` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Injective.under` `HomologicalComplex.X` `CategoryTheory.Limits.HasZeroMorphisms.zero`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`
`degreewiseEpiWithInjectiveKernel_p` 📖	mathematical	—	`CochainComplex.degreewiseEpiWithInjectiveKernel` `CategoryTheory.Limits.biprod` `CochainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `HomologicalComplex.instCategory` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `HomologicalComplex.instHasZeroMorphisms` `CochainComplex.mappingCone` `I` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `CategoryTheory.Abelian.hasBinaryBiproducts` `HomologicalComplex.X` `HomologicalComplex.instHasBinaryBiproduct` `p`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `CategoryTheory.Abelian.hasBinaryBiproducts` `HomologicalComplex.instHasBinaryBiproduct` `CategoryTheory.Abelian.epiWithInjectiveKernel_iff` `instInjectiveXIntMappingConeIdI` `CategoryTheory.Limits.BinaryBicone.inl_snd` `CategoryTheory.Limits.BinaryBicone.inl_fst` `CategoryTheory.Limits.BinaryBicone.inr_snd` `CategoryTheory.Limits.biprod.total`
`fac` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CochainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.instCategory` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Limits.biprod` `HomologicalComplex.instHasZeroMorphisms` `CochainComplex.mappingCone` `I` `CategoryTheory.CategoryStruct.id` `CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `CategoryTheory.Abelian.hasBinaryBiproducts` `HomologicalComplex.X` `HomologicalComplex.instHasBinaryBiproduct` `i` `p`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `CategoryTheory.Abelian.hasBinaryBiproducts` `HomologicalComplex.instHasBinaryBiproduct` `CategoryTheory.Limits.biprod.lift_snd`
`fac_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CochainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.instCategory` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Limits.biprod` `HomologicalComplex.instHasZeroMorphisms` `CochainComplex.mappingCone` `I` `CategoryTheory.CategoryStruct.id` `CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `CategoryTheory.Abelian.hasBinaryBiproducts` `HomologicalComplex.X` `HomologicalComplex.instHasBinaryBiproduct` `i` `p`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `CategoryTheory.Abelian.hasBinaryBiproducts` `HomologicalComplex.instHasBinaryBiproduct` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `fac`
`i_f_comp` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `CategoryTheory.Limits.biprod` `CochainComplex` `HomologicalComplex.instCategory` `HomologicalComplex.instHasZeroMorphisms` `CochainComplex.mappingCone` `I` `CategoryTheory.CategoryStruct.id` `CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `CategoryTheory.Abelian.hasBinaryBiproducts` `HomologicalComplex.instHasBinaryBiproduct` `HomologicalComplex.Hom.f` `i` `CategoryTheory.Limits.biprod.fst` `CochainComplex.HomComplex.Cochain.v` `CochainComplex.mappingCone.snd` `add_zero` `AddMonoid.toAddZeroClass` `Int.instAddMonoid` `CategoryTheory.Injective.ι`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `CategoryTheory.Abelian.hasBinaryBiproducts` `HomologicalComplex.instHasBinaryBiproduct` `add_zero` `HomologicalComplex.biprod_lift_fst_f_assoc` `CochainComplex.mappingCone.lift_f_snd_v` `CochainComplex.HomComplex.Cochain.ofHoms_v`
`i_f_comp_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `CategoryTheory.Limits.biprod` `CochainComplex` `HomologicalComplex.instCategory` `HomologicalComplex.instHasZeroMorphisms` `CochainComplex.mappingCone` `I` `CategoryTheory.CategoryStruct.id` `CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `CategoryTheory.Abelian.hasBinaryBiproducts` `HomologicalComplex.instHasBinaryBiproduct` `HomologicalComplex.Hom.f` `i` `CategoryTheory.Limits.biprod.fst` `CochainComplex.HomComplex.Cochain.v` `CochainComplex.mappingCone.snd` `add_zero` `AddMonoid.toAddZeroClass` `Int.instAddMonoid` `CategoryTheory.Injective.ι`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `CategoryTheory.Abelian.hasBinaryBiproducts` `HomologicalComplex.instHasBinaryBiproduct` `add_zero` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `i_f_comp`
`instInjectiveXIntI` 📖	mathematical	—	`CategoryTheory.Injective` `HomologicalComplex.X` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `I`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Injective.injective_under`
`instInjectiveXIntMappingConeIdI` 📖	mathematical	—	`CategoryTheory.Injective` `HomologicalComplex.X` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `CochainComplex.mappingCone` `I` `CategoryTheory.CategoryStruct.id` `CochainComplex` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.instCategory` `CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `CategoryTheory.Abelian.hasBinaryBiproducts`	—	`CategoryTheory.Injective.of_iso` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `CategoryTheory.Abelian.hasBinaryBiproducts` `CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Injective.instBiprod` `instInjectiveXIntI`
`instIsStrictlyGEBiprodIntMappingConeIdIOfHAddOfNat` 📖	mathematical	—	`CochainComplex.IsStrictlyGE` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.Limits.biprod` `CochainComplex` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `HomologicalComplex.instCategory` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `HomologicalComplex.instHasZeroMorphisms` `CochainComplex.mappingCone` `I` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `CategoryTheory.Abelian.hasBinaryBiproducts` `HomologicalComplex.X` `HomologicalComplex.instHasBinaryBiproduct`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `CategoryTheory.Abelian.hasBinaryBiproducts` `HomologicalComplex.instHasBinaryBiproduct` `CochainComplex.isStrictlyGE_iff` `CategoryTheory.Limits.IsZero.of_iso` `CategoryTheory.Functor.hasBinaryBiproduct_of_preserves` `HomologicalComplex.instPreservesZeroMorphismsEval` `HomologicalComplex.instPreservesBinaryBiproductEval` `CochainComplex.isZero_of_isStrictlyGE` `instIsStrictlyGEI`
`instIsStrictlyGEI` 📖	mathematical	—	`CochainComplex.IsStrictlyGE` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `I`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CochainComplex.isStrictlyGE_iff` `CategoryTheory.Injective.isZero_under` `CochainComplex.isZero_of_isStrictlyGE`
`instMonoFIntI` 📖	mathematical	—	`CategoryTheory.Mono` `HomologicalComplex.X` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `CategoryTheory.Limits.biprod` `CochainComplex` `HomologicalComplex.instCategory` `HomologicalComplex.instHasZeroMorphisms` `CochainComplex.mappingCone` `I` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `CategoryTheory.Abelian.hasBinaryBiproducts` `HomologicalComplex.instHasBinaryBiproduct` `HomologicalComplex.Hom.f` `i`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.mono_of_mono_fac` `CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `CategoryTheory.Abelian.hasBinaryBiproducts` `HomologicalComplex.instHasBinaryBiproduct` `add_zero` `CategoryTheory.Injective.ι_mono` `i_f_comp`
`instMonoIntI` 📖	mathematical	—	`CategoryTheory.Mono` `CochainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `HomologicalComplex.instCategory` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Limits.biprod` `HomologicalComplex.instHasZeroMorphisms` `CochainComplex.mappingCone` `I` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `CategoryTheory.Abelian.hasBinaryBiproducts` `HomologicalComplex.X` `HomologicalComplex.instHasBinaryBiproduct` `i`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `HomologicalComplex.mono_of_mono_f` `CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `CategoryTheory.Abelian.hasBinaryBiproducts` `HomologicalComplex.instHasBinaryBiproduct` `instMonoFIntI`
`instQuasiIsoIntP` 📖	mathematical	—	`QuasiIso` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `CategoryTheory.Limits.biprod` `CochainComplex` `HomologicalComplex.instCategory` `HomologicalComplex.instHasZeroMorphisms` `CochainComplex.mappingCone` `I` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `CategoryTheory.Abelian.hasBinaryBiproducts` `HomologicalComplex.X` `HomologicalComplex.instHasBinaryBiproduct` `p` `CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian` `HomologicalComplex.sc`	—	`HomotopyEquiv.quasiIso_hom` `AddRightCancelSemigroup.toIsRightCancelAdd` `CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `CategoryTheory.Abelian.hasBinaryBiproducts` `HomologicalComplex.instHasBinaryBiproduct` `CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian`

---

← Back to Index