Documentation Verification Report

Linear

📁 Source: Mathlib/Algebra/Homology/ShortComplex/Linear.lean

Statistics

Metric	Count
Definitions `smul`, `smul`, `smul`, `smul`, `instLinear`, `instModuleHom`, `instSMulHom`	7
Theorems `smul_left`, `smul_right`, `smul_h₀`, `smul_h₁`, `smul_h₂`, `smul_h₃`, `smul_φH`, `smul_φK`, `smul_φH`, `smul_φQ`, `cyclesFunctor_linear`, `cyclesMap'_smul`, `cyclesMap_smul`, `homologyFunctor_linear`, `homologyMap'_smul`, `homologyMap_smul`, `leftHomologyFunctor_linear`, `leftHomologyMap'_smul`, `leftHomologyMap_smul`, `opcyclesFunctor_linear`, `opcyclesMap'_smul`, `opcyclesMap_smul`, `rightHomologyFunctor_linear`, `rightHomologyMap'_smul`, `rightHomologyMap_smul`, `smul_τ₁`, `smul_τ₂`, `smul_τ₃`	28
Total	35

CategoryTheory.ShortComplex

Definitions

Name	Category	Theorems
`instLinear` 📖	CompOp	5 math math: `cyclesFunctor_linear`, `opcyclesFunctor_linear`, `rightHomologyFunctor_linear`, `homologyFunctor_linear`, `leftHomologyFunctor_linear`
`instModuleHom` 📖	CompOp	—
`instSMulHom` 📖	CompOp	23 math math: `opcyclesMap_smul`, `homologyMap_smul`, `Homotopy.smul_h₁`, `Homotopy.smul_h₂`, `LeftHomologyMapData.smul_φH`, `Homotopy.smul_h₀`, `Homotopy.smul_h₃`, `cyclesMap_smul`, `smul_τ₃`, `cyclesMap'_smul`, `RightHomologyMapData.smul_φH`, `homologyMap'_smul`, `HomologyMapData.smul_right`, `LeftHomologyMapData.smul_φK`, `RightHomologyMapData.smul_φQ`, `smul_τ₁`, `smul_τ₂`, `rightHomologyMap'_smul`, `rightHomologyMap_smul`, `HomologyMapData.smul_left`, `leftHomologyMap_smul`, `opcyclesMap'_smul`, `leftHomologyMap'_smul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cyclesFunctor_linear` 📖	mathematical	—	`CategoryTheory.Functor.Linear` `CategoryTheory.ShortComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `instCategory` `instPreadditive` `instLinear` `cyclesFunctor`	—	`cyclesMap_smul`
`cyclesMap'_smul` 📖	mathematical	—	`cyclesMap'` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `Quiver.Hom` `CategoryTheory.ShortComplex` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `instCategory` `instSMulHom` `LeftHomologyData.K` `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`	—	`LeftHomologyMapData.cyclesMap'_eq`
`cyclesMap_smul` 📖	mathematical	—	`cyclesMap` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `Quiver.Hom` `CategoryTheory.ShortComplex` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `instCategory` `instSMulHom` `cycles` `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`	—	`cyclesMap'_smul`
`homologyFunctor_linear` 📖	mathematical	—	`CategoryTheory.Functor.Linear` `CategoryTheory.ShortComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `instCategory` `instPreadditive` `instLinear` `homologyFunctor`	—	`CategoryTheory.CategoryWithHomology.hasHomology` `homologyMap_smul`
`homologyMap'_smul` 📖	mathematical	—	`homologyMap'` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `Quiver.Hom` `CategoryTheory.ShortComplex` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `instCategory` `instSMulHom` `LeftHomologyData.H` `HomologyData.left` `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`	—	`leftHomologyMap'_smul`
`homologyMap_smul` 📖	mathematical	—	`homologyMap` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `Quiver.Hom` `CategoryTheory.ShortComplex` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `instCategory` `instSMulHom` `homology` `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`	—	`homologyMap'_smul`
`leftHomologyFunctor_linear` 📖	mathematical	—	`CategoryTheory.Functor.Linear` `CategoryTheory.ShortComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `instCategory` `instPreadditive` `instLinear` `leftHomologyFunctor`	—	`leftHomologyMap_smul`
`leftHomologyMap'_smul` 📖	mathematical	—	`leftHomologyMap'` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `Quiver.Hom` `CategoryTheory.ShortComplex` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `instCategory` `instSMulHom` `LeftHomologyData.H` `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`	—	`LeftHomologyMapData.leftHomologyMap'_eq`
`leftHomologyMap_smul` 📖	mathematical	—	`leftHomologyMap` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `Quiver.Hom` `CategoryTheory.ShortComplex` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `instCategory` `instSMulHom` `leftHomology` `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`	—	`leftHomologyMap'_smul`
`opcyclesFunctor_linear` 📖	mathematical	—	`CategoryTheory.Functor.Linear` `CategoryTheory.ShortComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `instCategory` `instPreadditive` `instLinear` `opcyclesFunctor`	—	`opcyclesMap_smul`
`opcyclesMap'_smul` 📖	mathematical	—	`opcyclesMap'` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `Quiver.Hom` `CategoryTheory.ShortComplex` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `instCategory` `instSMulHom` `RightHomologyData.Q` `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`	—	`RightHomologyMapData.opcyclesMap'_eq`
`opcyclesMap_smul` 📖	mathematical	—	`opcyclesMap` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `Quiver.Hom` `CategoryTheory.ShortComplex` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `instCategory` `instSMulHom` `opcycles` `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`	—	`opcyclesMap'_smul`
`rightHomologyFunctor_linear` 📖	mathematical	—	`CategoryTheory.Functor.Linear` `CategoryTheory.ShortComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `instCategory` `instPreadditive` `instLinear` `rightHomologyFunctor`	—	`rightHomologyMap_smul`
`rightHomologyMap'_smul` 📖	mathematical	—	`rightHomologyMap'` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `Quiver.Hom` `CategoryTheory.ShortComplex` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `instCategory` `instSMulHom` `RightHomologyData.H` `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`	—	`RightHomologyMapData.rightHomologyMap'_eq`
`rightHomologyMap_smul` 📖	mathematical	—	`rightHomologyMap` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `Quiver.Hom` `CategoryTheory.ShortComplex` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `instCategory` `instSMulHom` `rightHomology` `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`	—	`rightHomologyMap'_smul`
`smul_τ₁` 📖	mathematical	—	`Hom.τ₁` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `Quiver.Hom` `CategoryTheory.ShortComplex` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `instCategory` `instSMulHom` `X₁` `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`	—	—
`smul_τ₂` 📖	mathematical	—	`Hom.τ₂` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `Quiver.Hom` `CategoryTheory.ShortComplex` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `instCategory` `instSMulHom` `X₂` `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`	—	—
`smul_τ₃` 📖	mathematical	—	`Hom.τ₃` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `Quiver.Hom` `CategoryTheory.ShortComplex` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `instCategory` `instSMulHom` `X₃` `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.ShortComplex.HomologyMapData

Definitions

Name	Category	Theorems
`smul` 📖	CompOp	2 math math: `smul_right`, `smul_left`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`smul_left` 📖	mathematical	—	`left` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `Quiver.Hom` `CategoryTheory.ShortComplex` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ShortComplex.instCategory` `CategoryTheory.ShortComplex.instSMulHom` `smul` `CategoryTheory.ShortComplex.LeftHomologyMapData.smul` `CategoryTheory.ShortComplex.HomologyData.left`	—	—
`smul_right` 📖	mathematical	—	`right` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `Quiver.Hom` `CategoryTheory.ShortComplex` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ShortComplex.instCategory` `CategoryTheory.ShortComplex.instSMulHom` `smul` `CategoryTheory.ShortComplex.RightHomologyMapData.smul` `CategoryTheory.ShortComplex.HomologyData.right`	—	—

CategoryTheory.ShortComplex.Homotopy

Definitions

Name	Category	Theorems
`smul` 📖	CompOp	4 math math: `smul_h₁`, `smul_h₂`, `smul_h₀`, `smul_h₃`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`smul_h₀` 📖	mathematical	—	`h₀` `Quiver.Hom` `CategoryTheory.ShortComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ShortComplex.instCategory` `CategoryTheory.ShortComplex.instSMulHom` `smul` `CategoryTheory.ShortComplex.X₁` `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`	—	—
`smul_h₁` 📖	mathematical	—	`h₁` `Quiver.Hom` `CategoryTheory.ShortComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ShortComplex.instCategory` `CategoryTheory.ShortComplex.instSMulHom` `smul` `CategoryTheory.ShortComplex.X₂` `CategoryTheory.ShortComplex.X₁` `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`	—	—
`smul_h₂` 📖	mathematical	—	`h₂` `Quiver.Hom` `CategoryTheory.ShortComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ShortComplex.instCategory` `CategoryTheory.ShortComplex.instSMulHom` `smul` `CategoryTheory.ShortComplex.X₃` `CategoryTheory.ShortComplex.X₂` `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`	—	—
`smul_h₃` 📖	mathematical	—	`h₃` `Quiver.Hom` `CategoryTheory.ShortComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ShortComplex.instCategory` `CategoryTheory.ShortComplex.instSMulHom` `smul` `CategoryTheory.ShortComplex.X₃` `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.ShortComplex.LeftHomologyMapData

Definitions

Name	Category	Theorems
`smul` 📖	CompOp	3 math math: `smul_φH`, `smul_φK`, `CategoryTheory.ShortComplex.HomologyMapData.smul_left`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`smul_φH` 📖	mathematical	—	`φH` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `Quiver.Hom` `CategoryTheory.ShortComplex` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ShortComplex.instCategory` `CategoryTheory.ShortComplex.instSMulHom` `smul` `CategoryTheory.ShortComplex.LeftHomologyData.H` `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`	—	—
`smul_φK` 📖	mathematical	—	`φK` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `Quiver.Hom` `CategoryTheory.ShortComplex` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ShortComplex.instCategory` `CategoryTheory.ShortComplex.instSMulHom` `smul` `CategoryTheory.ShortComplex.LeftHomologyData.K` `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.ShortComplex.RightHomologyMapData

Definitions

Name	Category	Theorems
`smul` 📖	CompOp	3 math math: `smul_φH`, `CategoryTheory.ShortComplex.HomologyMapData.smul_right`, `smul_φQ`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`smul_φH` 📖	mathematical	—	`φH` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `Quiver.Hom` `CategoryTheory.ShortComplex` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ShortComplex.instCategory` `CategoryTheory.ShortComplex.instSMulHom` `smul` `CategoryTheory.ShortComplex.RightHomologyData.H` `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`	—	—
`smul_φQ` 📖	mathematical	—	`φQ` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `Quiver.Hom` `CategoryTheory.ShortComplex` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ShortComplex.instCategory` `CategoryTheory.ShortComplex.instSMulHom` `smul` `CategoryTheory.ShortComplex.RightHomologyData.Q` `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`	—	—

---

← Back to Index