theorem Finsupp.linearCombination_eq_sum {α : Type u_1} {β : Type u_2} {ι : Type u_3} [Fintype ι] [AddCommMonoid α] [Semiring β] [Module β α] (v : ι → α) (y : ι →₀ β) : (linearCombination β v) y = ∑ j : ι, y j • v j