refactor(analysis/convex/combination): generalize linear_combination to semimodules

[YaelDillies]

std_simplex and finset.center_mass are currently only defined in real vector spaces. This generalizes ℝ to any arbitrary ordered_semiring.
Specifically, what I'm doing is

• renaming finset.center_mass to finset.linear_combination
• removing the division from its definition. This makes it a bilinear map, but it's not yet bundled. It also seems to simplify the proofs.
• replacing ℝ by 𝕜 along with ordered_semiring 𝕜 (or linear_ordered_field 𝕜 in some lemmas)
• swapping the two arguments p (indexed family of points) and w (weights) so that it matches finset.affine_combination.

---

There are some things that still need to be done:

• It's becoming clear that this file doesn't belong under analysis.convex. Any idea where it could go?
• Instead of taking s : finset ι and w : ι → 𝕜, we should use ι →₀ 𝕜.
• We should define convex_space. Then convex_combination will be the common generalization of linear_combination and affine_combination.

[eric-wieser]

renaming finset.center_mass to finset.linear_combination

This feels like an easy PR to split off to cut down the size of the diff. Is that a reasonable request?

Actually this description seems out of date.

[eric-wieser]

Does this actually exist any more? I just see .sum (w • p) below.

[YaelDillies]

I doubt this is a good idea anymore. We will eventually have both what I was trying to achieve here, namely an explicit sum formula, and abstract affine combinations. But removing the existing finset.center_mass does not seem like the best first step now that I used it for Stone's separation.