Documentation Verification Report

Linear

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

Statistics

Metric	Count
Definitions `module'`, `smul`, `linear`	3
Theorems `smul_eq`, `linear_functor`	2
Total	5

CategoryTheory.Quotient

Definitions

Name	Category	Theorems
`linear` 📖	CompOp	1 math math: `linear_functor`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`linear_functor` 📖	mathematical	`Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `CategoryTheory.Preadditive.homGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `CategoryTheory.Linear.homModule`	`CategoryTheory.Functor.Linear` `CategoryTheory.Quotient` `category` `linear` `functor`	—	—

CategoryTheory.Quotient.Linear

Definitions

Name	Category	Theorems
`module'` 📖	CompOp	—
`smul` 📖	CompOp	1 math math: `smul_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`smul_eq` 📖	mathematical	`Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `CategoryTheory.Preadditive.homGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `CategoryTheory.Linear.homModule`	`CategoryTheory.Quotient` `CategoryTheory.Quotient.category` `CategoryTheory.Functor.obj` `CategoryTheory.Quotient.functor` `smul` `CategoryTheory.Functor.map`	—	—

---

← Back to Index