Basic

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

Statistics

Metric	Count
Definitions degreewiseEpiWithInjectiveKernel	1
Theorems instIsMultiplicativeIntDegreewiseEpiWithInjectiveKernel	1
Total	2

CochainComplex

Definitions

Name	Category	Theorems
degreewiseEpiWithInjectiveKernel 📖	CompOp	2 math math: cm5b.degreewiseEpiWithInjectiveKernel_p, instIsMultiplicativeIntDegreewiseEpiWithInjectiveKernel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsMultiplicativeIntDegreewiseEpiWithInjectiveKernel 📖	mathematical	—	CategoryTheory.MorphismProperty.IsMultiplicative 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 degreewiseEpiWithInjectiveKernel	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.MorphismProperty.id_mem CategoryTheory.MorphismProperty.IsMultiplicative.toContainsIdentities CategoryTheory.Abelian.instIsMultiplicativeEpiWithInjectiveKernel CategoryTheory.MorphismProperty.comp_mem CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition

---

← Back to Index