Preadditive

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

Statistics

Metric	Count
Definitions	0
Theorems app_add, app_neg, app_sub	3
Total	3

CategoryTheory.CatCenter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
app_add 📖	mathematical	—	app CategoryTheory.CatCenter Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing CategoryTheory.Preadditive.instRingEnd CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.functorCategoryPreadditive CategoryTheory.Functor.id Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup	—	—
app_neg 📖	mathematical	—	app CategoryTheory.CatCenter NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.Preadditive.instAddCommGroupEnd CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.functorCategoryPreadditive CategoryTheory.Functor.id Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Preadditive.homGroup	—	—
app_sub 📖	mathematical	—	app CategoryTheory.CatCenter SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CategoryTheory.Preadditive.instRingEnd CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.functorCategoryPreadditive CategoryTheory.Functor.id Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup	—	—

---

← Back to Index