noncomputable def Prop2369_tensorRight_map_homotopy (R : Type u_1) [CommRing R] {ι : Type u_2} {c : ComplexShape ι} {C D : HomologicalComplex (ModuleCat R) c} {f g : C ⟶ D} (A : ModuleCat R) (h : Homotopy f g) : Homotopy (((CategoryTheory.MonoidalCategory.tensorRight A).mapHomologicalComplex c).map f) (((CategoryTheory.MonoidalCategory.tensorRight A).mapHomologicalComplex c).map g)