∀ {ι : Type u} {γ : Type w} {α : Option ι → Type v} [inst : (i : Option ι) → Zero (α i)]
  [inst_1 : (i : Option ι) → SMulZeroClass γ (α i)] (r : γ) (f : Π₀ (i : Option ι), α i),
  DFinsupp.equivProdDFinsupp (r • f) = r • DFinsupp.equivProdDFinsupp f