∀ {M : Type u_1} {A : Type u_3} {B : Type u_4} {C : Type u_5} [inst : Zero A] [inst_1 : Zero B] [inst_2 : Zero C]
  [inst_3 : SMulZeroClass M C] (m : M) (g : ZeroHom B C) (f : ZeroHom A B), (m • g).comp f = m • g.comp f