∀ {R : Type u} [inst : Semiring R] {ι : Type v} {M : ι → Type w} [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] [inst_3 : DecidableEq ι] [inst_4 : (i : ι) → (x : M i) → Decidable (x ≠ 0)]
  (c : R) (v : DirectSum ι fun i => M i), DFinsupp.support (c • v) ⊆ DFinsupp.support v