Integer multiples and the tensor product in a monoidal preadditive category

In a monoidal preadditive category the whiskerings are additive, so they commute with integer multiples of morphisms (Mathlib's Functor.map_zsmul for tensorLeft and tensorRight); hence so does the tensor product of morphisms in each variable. Mathlib's CategoryTheory.MonoidalPreadditive records the additivity (and CategoryTheory.MonoidalLinear the compatibility with scalars of a chosen ring), but not the ℤ-multiples every preadditive category carries. These are the signs of the simplicial boundary and of the Koszul rule, which have to be moved through tensor products of morphisms.

@[simp]

theorem CategoryTheory.zsmul_tensorHom {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [MonoidalCategory C] [MonoidalPreadditive C] {W X Y Z : C} (m : ℤ) (f : W ⟶ X) (g : Y ⟶ Z) : MonoidalCategoryStruct.tensorHom (m • f) g = m • MonoidalCategoryStruct.tensorHom f g

Tensoring morphisms commutes with integer scalar multiplication in the first variable.

@[simp]

theorem CategoryTheory.tensorHom_zsmul {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [MonoidalCategory C] [MonoidalPreadditive C] {W X Y Z : C} (m : ℤ) (f : W ⟶ X) (g : Y ⟶ Z) : MonoidalCategoryStruct.tensorHom f (m • g) = m • MonoidalCategoryStruct.tensorHom f g

Tensoring morphisms commutes with integer scalar multiplication in the second variable.