Preadditive

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

Statistics

Metric	Count
Definitions Preadditive, add, neg, preadditive	4
Theorems functor_additive	1
Total	5

CategoryTheory

Definitions

Name	Category	Theorems
Preadditive 📖	CompData	1 math math: subsingleton_preadditive_of_hasBinaryBiproducts

CategoryTheory.Quotient

Definitions

Name	Category	Theorems
preadditive 📖	CompOp	1 math math: functor_additive

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
functor_additive 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup	CategoryTheory.Functor.Additive CategoryTheory.Quotient category preadditive functor	—	—

CategoryTheory.Quotient.Preadditive

Definitions

Name	Category	Theorems
add 📖	CompOp	—
neg 📖	CompOp	—

---

← Back to Index