linearCombination

Stream: mathlib4

[Antoine Chambert-Loir]

There is a slight inconsistency in the definition of docs#Finsupp.linearCombination and docs#Fintype.linearCombination. Both take a family of scalars $c:\alpha \to R$ and a family of vectors $v:\alpha \to M$ and produce the linear combination $\sum_{a\in\alpha} c(a) \bullet v(a)$. The first difference (expressed by the namespace) is that the first one assumes $c$ to be finitely supported, while the second the second assumes that $\alpha$ is a finite type. The second difference is that the second insures bilinearity on the two variables $c$ and $v$, hence requires that $R$ is commutative.

I wonder whether one shouldn't align both definitions.
My impression is that both are needed, and one needs to choose which one would be linearCombinationand which one would have a new name, and which name?