Finitely supported product

Stream: maths

[Yaël Dillies]

docs#finsupp.prod returns the product of a finsupp over all nonzero values. But isn't that bit weird compared to docs#finsupp.sum? finsupp.sum is literally the sum of all values of a finitely supported function, but the product isn't. Are we missing α →₁ β the multiplicative version of α →₀ β, or does it simply not turn up anywhere?

[Yaël Dillies]

In particular, finsupp.prod is always nonzero (when we have docs#no_zero_divisors).

[Yakov Pechersky]

There's docs#set.mul_indicator that gets used in finprod

[Eric Wieser]

I don't think sum is any weirder than prod; f.sum g is weird on any map that doesn't satisfy g 0 = 0, while f.prod g is weird on any map that doesn't satisfy g 0 = 1