Vanishing transport through the module tensor product

The relative tensor product of modules vanishes when either factor does: the projection from the ordinary tensor product is epic, and the ordinary tensor product with a zero object is zero.

theorem RS.isZero_modTensor_left {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasCoequalizers D] (A : D) [CategoryTheory.MonObj A] (M N : CategoryTheory.Mod D A) (h : CategoryTheory.Limits.IsZero M.X) : CategoryTheory.Limits.IsZero (modTensor A M N)

The module tensor product of a zero module vanishes, left-factor version.