∀ (R : Type u_1) (M : Type u_2) [inst : Ring R] [IsDomain R] [inst_2 : AddCommGroup M] [inst_3 : Module R M]
  [Module.IsTorsionFree R M] (x : M), x ≠ 0 → Function.Injective ⇑(LinearMap.toSpanSingleton R M x)