∀ {R : Type u_1} (M : Type u_3) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {r : R}
  [Module.IsTorsionFree R M] [IsCancelMulZero R], r ≠ 0 → Function.Injective fun x => r • x