Indization

📁 Source: Mathlib/CategoryTheory/Preadditive/Indization.lean

Statistics

Metric	Count
Definitions instPreadditiveInd	1
Theorems instHasFiniteBiproductsInd	1
Total	2

CategoryTheory

Definitions

Name	Category	Theorems
instPreadditiveInd 📖	CompOp	2 math math: instIsIsoIndCoimageImageComparison, instHasFiniteBiproductsInd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instHasFiniteBiproductsInd 📖	mathematical	—	Limits.HasFiniteBiproducts Ind instCategoryInd Preadditive.preadditiveHasZeroMorphisms instPreadditiveInd	—	Limits.HasFiniteBiproducts.of_hasFiniteCoproducts Limits.hasFiniteCoproducts_of_hasFiniteColimits Limits.hasFiniteColimits_of_hasColimits instHasColimitsIndOfHasFiniteColimits

---

← Back to Index