∀ {Γ : Type u_1} {V : Type u_2} [inst : PartialOrder Γ] [inst_1 : AddCommMonoid V] (g : Γ) (x y : HahnSeries Γ V),
  (↑(HahnSeries.coeff.addMonoidHom g)).toFun (x + y) =
    (↑(HahnSeries.coeff.addMonoidHom g)).toFun x + (↑(HahnSeries.coeff.addMonoidHom g)).toFun y