finsupp.{prod,sum}

Stream: general

[Johan Commelin]

Do people like finsupp.prod and finsupp.sum? I feel like they are one layer too much in the hierarchy
list.prod -> multiset.prod -> finset.prod -> finsupp.prod.
Should we try to completely remove them, and use finset.prod instead? Or is this doomed to begin with?

[Johan Commelin]

I also suggest

def weight (f : ι →₀ A) : A :=
∑ i in f.support, f i

[Patrick Massot]

What's this name?

[Patrick Massot]

Why not sum?

[Johan Commelin]

Ok, we could reuse finsupp.sum for that notion, once we free up the name.