Finsupp.sum_smul_index

Stream: Is there code for X?

[Antoine Chambert-Loir]

The present version of docs#Finsupp.sum_smul_index' can be generalized to

-- Generalizes `Finsupp.sum_smul_index'`
example  {R M N : Type*} [Semiring R]
    [AddCommMonoid M] [Module R M] [AddCommMonoid N]
    {f : ι →₀ M} {r : R} {g : ι → M → N}
    (h0 : ∀ i ∈ f.support, g i 0 = 0) :
    (Finsupp.sum (r • f) g) = Finsupp.sum f (fun i m => g i (r • m)) := by
  apply symm
  rw [Finsupp.sum, Finsupp.sum_of_support_subset _ Finsupp.support_smul _ h0]
  apply Finset.sum_congr rfl
  · intro i _
    simp only [Finsupp.coe_smul, Pi.smul_apply]

but the proof is longer than the one-line initial proof exact Finsupp.sum_mapRange_index h0.

[Eric Wieser]

That's not more general, the version in mathlib assumes only DistribSMul R M

[Antoine Chambert-Loir]

I think it is because of f which is valued in R…

[Eric Wieser]

You're comparing to

theorem sum_smul_index' [AddMonoid M] [DistribSMul R M] [AddCommMonoid N] {g : α →₀ M} {b : R}
    {h : α → M → N} (h0 : ∀ i, h i 0 = 0) : (b • g).sum h = g.sum fun i c => h i (b • c) :=
  Finsupp.sum_mapRange_index h0

right?

[Antoine Chambert-Loir]

But no, I'm confusing with docs#Finsupp.sum_smul_index (not primed)

[Antoine Chambert-Loir]

So yes, I should have!

[Eric Wieser]

I guess your intended generalization is ∈ f.support?

[Antoine Chambert-Loir]

I really meant for the monoid value.
I don't know whether the ∈ f.support is important, I wrote it inconsciously…

[Eric Wieser]

I think it's a good generalization, since we had a PR not that long ago that added it to sum_add_index

[Antoine Chambert-Loir]

I should make it in another PR, here, I'm doing tensor products…

[Eric Wieser]

Presumably then the existing primed lemma already has the generalization you wanted?

[Eric Wieser]

Maybe the unprimed one should have a docstring that says its the special case of the primed one

[Antoine Chambert-Loir]

The primed lemma suffices me.
And the generalization for support can't be proved in one line, unless one generalizes docs#Finsupp.sum_mapRange_index.