∀ {R : Type u_3} {Γ : Type u_6} {V : Type u_7} [inst : Ring R] [IsDomain R] [inst_2 : AddCommGroup V]
  [inst_3 : AddCommMonoid Γ] [inst_4 : LinearOrder Γ] [inst_5 : IsOrderedCancelAddMonoid Γ] [inst_6 : Module R V]
  [Module.IsTorsionFree R V], Module.IsTorsionFree (HahnSeries Γ R) (HahnModule Γ R V)