Documentation Verification Report

Linear

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

Statistics

Metric	Count
Definitions `homModuleOfRingMorphism`, `ofRingMorphism`, `smulOfRingMorphism`, `toCatCenter`	4
Theorems `smulOfRingMorphism_smul_eq`, `smulOfRingMorphism_smul_eq'`, `toCatCenter_apply_app`	3
Total	7

CategoryTheory.Linear

Definitions

Name	Category	Theorems
`homModuleOfRingMorphism` 📖	CompOp	—
`ofRingMorphism` 📖	CompOp	—
`smulOfRingMorphism` 📖	CompOp	2 math math: `smulOfRingMorphism_smul_eq'`, `smulOfRingMorphism_smul_eq`
`toCatCenter` 📖	CompOp	1 math math: `toCatCenter_apply_app`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`smulOfRingMorphism_smul_eq` 📖	mathematical	—	`Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `smulOfRingMorphism` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.CatCenter.app` `DFunLike.coe` `RingHom` `CategoryTheory.CatCenter` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `CategoryTheory.Preadditive.instSemiringEnd` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.functorCategoryPreadditive` `CategoryTheory.Functor.id` `RingHom.instFunLike`	—	—
`smulOfRingMorphism_smul_eq'` 📖	mathematical	—	`Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `smulOfRingMorphism` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.CatCenter.app` `DFunLike.coe` `RingHom` `CategoryTheory.CatCenter` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `CategoryTheory.Preadditive.instSemiringEnd` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.functorCategoryPreadditive` `CategoryTheory.Functor.id` `RingHom.instFunLike`	—	`smulOfRingMorphism_smul_eq` `CategoryTheory.CatCenter.naturality`
`toCatCenter_apply_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.id` `DFunLike.coe` `RingHom` `CategoryTheory.CatCenter` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `CategoryTheory.Preadditive.instSemiringEnd` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.functorCategoryPreadditive` `RingHom.instFunLike` `toCatCenter` `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` `homModule` `CategoryTheory.CategoryStruct.id`	—	—

---

← Back to Index