Sum of terms of a finsupp function

Stream: Is there code for X?

[Antoine Chambert-Loir]

When working with multivariate polynomials or multivariate power series, it is often necessary to consider the sum of all terms of a finitely supported function d : I -> Nat, and to know basic things such as the fact as the sum is 0 if and only if d = 0.
Obviously, most definitions and results apply when Nat is replaced by a reasonable AddCommMonoid…
The theory of degree of polynomials contains docs#MvPolynomial.weightedDegree which
should probably be accessible in another file, under another name…

Any idea of where to put it and in what generality?

[Yaël Dillies]

Can't you simply write ∑ i, d i?

[Antoine Chambert-Loir]

I certainly can, but my experience is that for some proofs, that makes it simpler to have a name for this function of d. (Some mathematicians would write it |d|.)

[Ruben Van de Velde]

Do we not have docs#Finsupp.sum ?

[Antoine Chambert-Loir]

Using docs#Finsupp.sum, one has to type d.sum (fun _ => id) every time, which is relatively unappealing.

[Yaël Dillies]

I think this is a case where you should just have local notation, eg |d|

[Antoine Chambert-Loir]

Updating Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous to use such a local notation (that needs to be used elsewhere; probably a scoped notationis possible, but in what scope?) looks frightening to me…

[Antoine Chambert-Loir]

Finsupp.total _ _ _ 1 d also works, and there is quite an API for docs#Finsupp.total, but these three underscores are also annoying.