∀ {Γ : Type u_1} (R : Type u_3) {V : Type u_2} [inst : PartialOrder Γ] [inst_1 : Semiring R] [inst_2 : AddCommMonoid V]
  [inst_3 : Module R V] (x : R) (x_1 : Γ →₀ V),
  HahnSeries.ofFinsupp (x • x_1) = (RingHom.id R) x • HahnSeries.ofFinsupp x_1