∀ {M : Type u_4} {N : Type u_5} [inst : AddMonoid M] [inst_1 : AddZeroClass N] [inst_2 : AddAction M N]
  [inst_3 : VAddAssocClass M N N],
  AddMonoidHom.vaddZeroHom = { toFun := fun x => x +ᵥ 0, map_zero' := ⋯, map_add' := ⋯ }