finset.center_mass as a linear map

Stream: Is there code for X?

[Yaël Dillies]

I'm trying to redefine docs#finset.center_mass as a linear map.

def finset.center_mass {𝕜 E : Type*} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E]
  (s : finset ι) (p : ι → E) :
  (ι → 𝕜) →ₗ[𝕜] E :=
⟨λ w, ∑ i in s, w i • p i, ???⟩

I'm completely clueless about the names of the bundled linear maps I need. What are they? Maybe docs#linear_map.smul_right is close?

[Yury G. Kudryashov]

I suggest that you use docs#finsupp and docs#finsupp.lift

[Yury G. Kudryashov]

No, wrong bundled version.

[Yury G. Kudryashov]

I'm surprised that we don't have a more bundled version of docs#finsupp.total