Refinements

Statistics

Metric	Count
Definitions	0
Theorems `eq_liftCycles_homologyπ_up_to_refinements`	1
Total	1

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_liftCycles_homologyπ_up_to_refinements` 📖	mathematical	`ComplexShape.next`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `homology` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian` `sc` `cycles` `liftCycles` `homologyπ`	—	`CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian` `CategoryTheory.ShortComplex.eq_liftCycles_homologyπ_up_to_refinements`

---