DFinsupp.sum_smul_index missing

Stream: mathlib4

[Daniel Weber]

DFinsupp has some sum_X_index lemmas, like Finsupp, for example docs#DFinsupp.sum_add_index (compare to docs#Finsupp.sum_add_index), but the counterpart for docs#Finsupp.sum_smul_index seems to be missing.
Is there some reason for that, or should it be added?

[Yury G. Kudryashov]

My guess: the only reason is that no one needed it up until now.

[Yury G. Kudryashov]

So, please PR it!

[Daniel Weber]

Where should this result be placed?

import Mathlib

variable {δ ι γ : Type*} {β : ι → Type*} [DecidableEq ι]

theorem DFinsupp.sum_smul_index [∀ i, AddMonoid (β i)] [Monoid δ] [∀ i, DistribMulAction δ (β i)] [∀ (i) (x : β i), Decidable (x ≠ 0)] [AddCommMonoid γ]
    {g : Π₀ i, β i} {b : δ} {h : ∀ i, β i → γ} (h0 : ∀ i, h i 0 = 0) :
    (b • g).sum h = g.sum fun i a => h i (b • a) :=
  sum_mapRange_index h0

/--
info: [Mathlib.Algebra.DirectSum.Basic,
 Mathlib.Data.DFinsupp.Interval,
 Mathlib.Data.DFinsupp.Multiset,
 Mathlib.LinearAlgebra.DFinsupp]
-/
#guard_msgs in
#find_home DFinsupp.sum_smul_index

[Kim Morrison]

How is this pulling in Mathlib.Algebra.DirectSum.Basic? That seems weird.

[Eric Wieser]

It works fine without the import

[Eric Wieser]

find_home still suggests it after replacing the proof with sorry, and

#eval Lean.Expr.getUsedConstants q(type_of% @DFinsupp.sum_smul_index.{0,0,0,0})

doesn't mention DirectSum

[Daniel Weber]

It's probably because it imports both sum and smul

[Eric Wieser]

Ah, I think Kim and I were confusing this with min_imports?

[Kim Morrison]

Ah, indeed. If this statement can happily live in Mathlib.LinearAlgebra.DFinsupp that seems the most natural out of those four.

[Eric Wieser]

Arguably we should create Mathlib.Algebra.BigOperators.DFinsupp for parity with Finsupp

[Eric Wieser]

But that could be a follow-up CL.